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

  val setup: theory -> theory

  val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state

  val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state

  val register_predicate : (string * thm list * thm * int) -> theory -> theory

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

  val is_registered : theory -> string -> bool

  val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm

  val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm

  val predfun_name_of: theory -> string -> Predicate_Compile_Aux.mode -> string

  val all_preds_of : theory -> string list

  val modes_of: theory -> string -> Predicate_Compile_Aux.mode list

  val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list

  val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string

  val generator_modes_of: theory -> string -> Predicate_Compile_Aux.mode list

  val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string

  val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list

  val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list

  val intros_of: theory -> string -> thm list

  val nparams_of: theory -> string -> int

  val add_intro: thm -> theory -> theory

  val set_elim: thm -> theory -> theory

  val set_nparams : string -> int -> theory -> theory

  val print_stored_rules: theory -> unit

  val print_all_modes: theory -> unit

  val mk_casesrule : Proof.context -> term -> int -> 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 code_pred_intros_attrib : attribute

  (* used by Quickcheck_Generator *) 

  (* temporary for testing of the compilation *)

  datatype compilation_funs = CompilationFuns of {

    mk_predT : typ -> typ,

    dest_predT : typ -> typ,

    mk_bot : typ -> term,

    mk_single : term -> term,

    mk_bind : term * term -> term,

    mk_sup : term * term -> term,

    mk_if : term -> term,

    mk_not : term -> term,

    mk_map : typ -> typ -> term -> term -> term

  };

  val pred_compfuns : compilation_funs

  val randompred_compfuns : compilation_funs

  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory

  val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory

  val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory

end;

structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =

struct

open Predicate_Compile_Aux;

(** auxiliary **)

(* debug stuff *)

fun print_tac s = Seq.single;

fun print_tac' options s = 

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

fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)

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 error ("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)));

(* reference to preprocessing of InductiveSet package *)

val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*)

(** 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 ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T

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

(* destruction of intro rules *)

(* FIXME: look for other place where this functionality was used before *)

fun strip_intro_concl nparams intro = let

  val _ $ u = Logic.strip_imp_concl intro

  val (pred, all_args) = strip_comb u

  val (params, args) = chop nparams all_args

in (pred, (params, args)) end

(** data structures **)

(* new datatype for modes: *)

(*

datatype instantiation = Input | Output

type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode

type mode = arg_mode list

type tmode = Mode of mode * 

*)

fun gen_split_smode (mk_tuple, strip_tuple) smode ts =

  let

    fun split_tuple' _ _ [] = ([], [])

    | split_tuple' is i (t::ts) =

      (if i mem is then apfst else apsnd) (cons t)

        (split_tuple' is (i+1) ts)

    fun split_tuple is t = split_tuple' is 1 (strip_tuple t)

    fun split_smode' _ _ [] = ([], [])

      | split_smode' smode i (t::ts) =

        (if i mem (map fst smode) then

          case (the (AList.lookup (op =) smode i)) of

            NONE => apfst (cons t)

            | SOME is =>

              let

                val (ts1, ts2) = split_tuple is t

                fun cons_tuple ts = if null ts then I else cons (mk_tuple ts)

                in (apfst (cons_tuple ts1)) o (apsnd (cons_tuple ts2)) end

          else apsnd (cons t))

        (split_smode' smode (i+1) ts)

  in split_smode' smode 1 ts end

fun split_smode smode ts = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple) smode ts

fun split_smodeT smode ts = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT) smode ts

fun gen_split_mode split_smode (iss, is) ts =

  let

    val (t1, t2) = chop (length iss) ts 

  in (t1, split_smode is t2) end

fun split_mode (iss, is) ts = gen_split_mode split_smode (iss, is) ts

fun split_modeT (iss, is) ts = gen_split_mode split_smodeT (iss, is) ts

datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term

  | Generator of (string * typ);

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

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

datatype predfun_data = PredfunData of {

  name : string,

  definition : thm,

  intro : thm,

  elim : thm

};

fun rep_predfun_data (PredfunData data) = data;

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

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

datatype function_data = FunctionData of {

  name : string,

  equation : thm option (* is not used at all? *)

};

fun rep_function_data (FunctionData data) = data;

fun mk_function_data (name, equation) =

  FunctionData {name = name, equation = equation}

datatype pred_data = PredData of {

  intros : thm list,

  elim : thm option,

  nparams : int,

  functions : (mode * predfun_data) list,

  generators : (mode * function_data) list,

  depth_limited_functions : (mode * function_data) list 

};

fun rep_pred_data (PredData data) = data;

fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) =

  PredData {intros = intros, elim = elim, nparams = nparams,

    functions = functions, generators = generators, depth_limited_functions = depth_limited_functions}

fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) =

  mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions)))

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) andalso

  #nparams d1 = #nparams d2

structure PredData = TheoryDataFun

(

  type T = pred_data Graph.T;

  val empty = Graph.empty;

  val copy = I;

  val extend = I;

  fun merge _ = Graph.merge eq_pred_data;

);

(* queries *)

fun lookup_pred_data thy name =

  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)

fun the_pred_data thy name = case lookup_pred_data thy 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

fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy

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

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

  | SOME thm => Thm.transfer thy thm 

val has_elim = is_some o #elim oo the_pred_data;

val nparams_of = #nparams oo the_pred_data

val modes_of = (map fst) o #functions oo the_pred_data

val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data

val random_modes_of = (map fst) o #generators oo the_pred_data

fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) 

val is_compiled = not o null o #functions oo the_pred_data

fun lookup_predfun_data thy name mode =

  Option.map rep_predfun_data (AList.lookup (op =)

  (#functions (the_pred_data thy name)) mode)

fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode

  of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)

   | SOME data => data;

val predfun_name_of = #name ooo the_predfun_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

fun lookup_generator_data thy name mode = 

  Option.map rep_function_data (AList.lookup (op =)

  (#generators (the_pred_data thy name)) mode)

fun the_generator_data thy name mode = case lookup_generator_data thy name mode

  of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)

   | SOME data => data

val generator_name_of = #name ooo the_generator_data

val generator_modes_of = (map fst) o #generators oo the_pred_data

fun all_generator_modes_of thy =

  map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) 

fun lookup_depth_limited_function_data thy name mode =

  Option.map rep_function_data (AList.lookup (op =)

  (#depth_limited_functions (the_pred_data thy name)) mode)

fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode

  of NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode

    ^ " of predicate " ^ name)

   | SOME data => data

val depth_limited_function_name_of = #name ooo the_depth_limited_function_data

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

        string_of_mode ms)) modes))

  else ()

fun print_pred_mode_table string_of_entry thy 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 string_of_prem thy (Prem (ts, p)) =

    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(premise)"

  | string_of_prem thy (Negprem (ts, p)) =

    (Syntax.string_of_term_global thy (HOLogic.mk_not (list_comb (p, ts)))) ^ "(negative premise)"

  | string_of_prem thy (Sidecond t) =

    (Syntax.string_of_term_global thy t) ^ "(sidecondition)"

  | string_of_prem thy _ = error "string_of_prem: unexpected input"

fun string_of_moded_prem thy (Prem (ts, p), tmode) =

    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^

    "(" ^ (string_of_tmode tmode) ^ ")"

  | string_of_moded_prem thy (Generator (v, T), _) =

    "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)

  | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =

    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^

    "(negative mode: " ^ string_of_smode is ^ ")"

  | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =

    (Syntax.string_of_term_global thy t) ^

    "(sidecond mode: " ^ string_of_smode is ^ ")"    

  | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"

fun print_moded_clauses thy =

  let

    fun string_of_clause pred mode clauses =

      cat_lines (map (fn (ts, prems) => (space_implode " --> "

        (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "

        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)

  in print_pred_mode_table string_of_clause thy end;

fun string_of_clause thy pred (ts, prems) =

  (space_implode " --> "

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

   ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))

fun print_compiled_terms options thy =

  if show_compilation options then

    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy

  else K ()

fun print_stored_rules thy =

  let

    val preds = (Graph.keys o PredData.get) thy

    fun print pred () = let

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

      val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))

      val _ = writeln ("introrules: ")

      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))

        (rev (intros_of thy pred)) ()

    in

      if (has_elim thy pred) then

        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))

      else

        writeln ("no elimrule defined")

    end

  in

    fold print preds ()

  end;

fun print_all_modes thy =

  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 thy) ()

  end

(* validity checks *)

fun check_expected_modes (options : Predicate_Compile_Aux.options) modes =

  case expected_modes options of

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

      SOME modes =>

        if not (eq_set (op =) (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 ()

      | 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 [] 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 nparams [] ctxt =

  let

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

    val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred))

    val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i))

      (1 upto nparams)) ctxt'

    val params = map Free (param_names ~~ paramTs)

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

  | import_intros inp_pred nparams (th :: ths) ctxt =

    let

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

      val thy = ProofContext.theory_of ctxt'

      val (pred, (params, args)) = strip_intro_concl nparams (prop_of th')

      val ho_args = filter (is_predT o fastype_of) 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 0 (prop_of th)

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

            error "Trying to instantiate another predicate" else ()

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

      fun instantiate_ho_args th =

        let

          val (_, (params', args')) = strip_intro_concl nparams (prop_of th)

          val ho_args' = map dest_Var (filter (is_predT o fastype_of) args')

        in Thm.certify_instantiate ([], map dest_Var params' ~~ params) 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, params), th' :: ths'), ctxt1)

    end

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

fun mk_casesrule ctxt pred nparams introrules =

  let

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

    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) = chop nparams (binder_types (fastype_of pred))

    val (argnames, ctxt3) = Variable.variant_fixes

      (map (fn i => "a" ^ string_of_int i) (1 upto length argsT)) ctxt2

    val argvs = map2 (curry Free) argnames argsT

    fun mk_case intro =

      let

        val (_, (_, args)) = strip_intro_concl nparams intro

        val prems = Logic.strip_imp_prems intro

        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)

        val frees = (fold o fold_aterms)

          (fn t as Free _ =>

              if member (op aconv) params t then I else insert (op aconv) t

           | _ => I) (args @ prems) []

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

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

    val cases = map mk_case intros

  in Logic.list_implies (assm :: cases, prop) 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 ("Trueprop", _) $ _ => Conv.arg_conv cv ct  

  | _ => error "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 thy nparams elimrule =

  let

    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =

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

     | replace_eqs t = t

    val ctxt = ProofContext.init thy

    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)))) - nparams

    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;

(* special case: predicate with no introduction rule *)

fun noclause thy predname elim = let

  val T = (Logic.unvarifyT o Sign.the_const_type thy) predname

  val Ts = binder_types T

  val names = Name.variant_list []

        (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts)))

  val vs = map2 (curry Free) names Ts

  val clausehd = HOLogic.mk_Trueprop (list_comb (Const (predname, T), vs))

  val intro_t = Logic.mk_implies (@{prop False}, clausehd)

  val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))

  val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)

  val intro = Goal.prove (ProofContext.init thy) names [] intro_t

        (fn _ => etac @{thm FalseE} 1)

  val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t

        (fn _ => etac elim 1) 

in

  ([intro], elim)

end

fun expand_tuples_elim th = th

fun fetch_pred_data thy name =

  case try (Inductive.the_inductive (ProofContext.init thy)) 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 intros = ind_set_codegen_preproc thy

          (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 = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams 

          (expand_tuples_elim pre_elim))*)

        val elim =

          (Drule.standard o Skip_Proof.make_thm thy)

          (mk_casesrule (ProofContext.init thy) pred nparams intros)

        val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)

      in

        mk_pred_data ((intros, SOME elim, nparams), ([], [], []))

      end                                                                    

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

(* updaters *)

fun apfst3 f (x, y, z) =  (f x, y, z)

fun apsnd3 f (x, y, z) =  (x, f y, z)

fun aptrd3 f (x, y, z) =  (x, y, f z)

fun add_predfun name mode data =

  let

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

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

fun is_inductive_predicate thy name =

  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)

fun depending_preds_of thy (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 thy c orelse is_registered thy c))

  end;

(* code dependency graph *)

(*

fun dependencies_of thy name =

  let

    val (intros, elim, nparams) = fetch_pred_data thy name 

    val data = mk_pred_data ((intros, SOME elim, nparams), ([], [], []))

    val keys = depending_preds_of thy intros

  in

    (data, keys)

  end;

*)

(* guessing number of parameters *)

fun find_indexes pred xs =

  let

    fun find is n [] = is

      | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;

  in rev (find [] 0 xs) end;

fun guess_nparams T =

  let

    val argTs = binder_types T

    val nparams = fold Integer.max

      (map (fn x => x + 1) (find_indexes is_predT argTs)) 0

  in nparams end;

fun add_intro thm thy = let

   val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of 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, nparams) => (intros @ [thm], elim, nparams)))) gr

     | NONE =>

       let

         val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)

       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end;

  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, _, nparams) = (intros, SOME thm, nparams)  

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

fun set_nparams name nparams = let

    fun set (intros, elim, _ ) = (intros, elim, nparams) 

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

fun register_predicate (constname, pre_intros, pre_elim, nparams) thy =

  let

    (* preprocessing *)

    val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)

    val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams 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, nparams), ([], [], [])))) 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 0 (prop_of 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 nparams = guess_nparams T

    val pre_elim = 

      (Drule.standard o Skip_Proof.make_thm thy)

      (mk_casesrule (ProofContext.init thy) pred nparams pre_intros)

  in register_predicate (constname, pre_intros, pre_elim, nparams) thy end

fun set_generator_name pred mode name = 

  let

    val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))

  in

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

  end

fun set_depth_limited_function_name pred mode name = 

  let

    val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))

  in

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

  end

datatype compilation_funs = CompilationFuns of {

  mk_predT : typ -> typ,

  dest_predT : typ -> typ,

  mk_bot : typ -> term,

  mk_single : term -> term,

  mk_bind : term * term -> term,

  mk_sup : term * term -> term,

  mk_if : term -> term,

  mk_not : term -> term,

  mk_map : typ -> typ -> term -> term -> term

};

fun mk_predT (CompilationFuns funs) = #mk_predT funs

fun dest_predT (CompilationFuns funs) = #dest_predT funs

fun mk_bot (CompilationFuns funs) = #mk_bot funs

fun mk_single (CompilationFuns funs) = #mk_single funs

fun mk_bind (CompilationFuns funs) = #mk_bind funs

fun mk_sup (CompilationFuns funs) = #mk_sup funs

fun mk_if (CompilationFuns funs) = #mk_if funs

fun mk_not (CompilationFuns funs) = #mk_not funs

fun mk_map (CompilationFuns funs) = #mk_map funs

fun funT_of compfuns (iss, is) T =

  let

    val Ts = binder_types T

    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts

    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs

  in

    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))

  end;

fun mk_fun_of compfuns thy (name, T) mode = 

  Const (predfun_name_of thy name mode, funT_of compfuns mode T)

structure PredicateCompFuns =

struct

fun mk_predT T = Type (@{type_name Predicate.pred}, [T])

fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T

  | dest_predT T = raise TYPE ("dest_predT", [T], []);

fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);

fun mk_single t =

  let val T = fastype_of t

  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;

fun mk_bind (x, f) =

  let val T as Type ("fun", [_, U]) = fastype_of f

  in

    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f

  end;

val mk_sup = HOLogic.mk_binop @{const_name sup};

fun mk_if cond = Const (@{const_name Predicate.if_pred},

  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;

fun mk_not t = let val T = mk_predT HOLogic.unitT

  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end

fun mk_Enum f =

  let val T as Type ("fun", [T', _]) = fastype_of f

  in

    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    

  end;

fun mk_Eval (f, x) =

  let

    val T = fastype_of x

  in

    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x

  end;

fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},

  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;

val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,

  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,

  mk_map = mk_map};

end;

structure RandomPredCompFuns =

struct

fun mk_randompredT T =

  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})

fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},

  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T

  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);

fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)

fun mk_single t =

  let

    val T = fastype_of t

  in

    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t

  end;

fun mk_bind (x, f) =

  let

    val T as (Type ("fun", [_, U])) = fastype_of f

  in

    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f

  end

val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}

fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},

  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;

fun mk_not t = let val T = mk_randompredT HOLogic.unitT

  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end

fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},

  (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp

val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot,

    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,

    mk_map = mk_map};

end;

(* for external use with interactive mode *)

val pred_compfuns = PredicateCompFuns.compfuns

val randompred_compfuns = RandomPredCompFuns.compfuns;

fun lift_random random =

  let

    val T = dest_randomT (fastype_of random)

  in

    Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} -->

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

      RandomPredCompFuns.mk_randompredT T) $ random

  end;

fun depth_limited_funT_of compfuns (iss, is) T =

  let

    val Ts = binder_types T

    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts

    val paramTs' = map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs 

  in

    (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}])

      ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))

  end;  

fun mk_depth_limited_fun_of compfuns thy (name, T) mode =

  Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)

fun mk_generator_of compfuns thy (name, T) mode = 

  Const (generator_name_of thy name mode, depth_limited_funT_of compfuns mode T)

(* Mode analysis *)

(*** check if a term contains only constructor functions ***)

fun is_constrt thy =

  let

    val cnstrs = flat (maps

      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)

      (Symtab.dest (Datatype.get_all thy)));

    fun check t = (case strip_comb t of

        (Free _, []) => true

      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of

            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts

          | _ => false)

      | _ => false)

  in check end;

(*** check if a type is an equality type (i.e. doesn't contain fun)

  FIXME this is only an approximation ***)

fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts

  | is_eqT _ = true;

fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];

val terms_vs = distinct (op =) o maps term_vs;

(** collect all Frees in a term (with duplicates!) **)

fun term_vTs tm =

  fold_aterms (fn Free xT => cons xT | _ => I) tm [];

fun subsets i j =

  if i <= j then

    let

      fun merge xs [] = xs

        | merge [] ys = ys

        | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)

            else y::merge (x::xs) ys;

      val is = subsets (i+1) j

    in merge (map (fn ks => i::ks) is) is end

  else [[]];

(* FIXME: should be in library - cprod = map_prod I *)

fun cprod ([], ys) = []

  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);

fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;

fun cprods_subset [] = [[]]

  | cprods_subset (xs :: xss) =

  let

    val yss = (cprods_subset xss)

  in maps (fn ys => map (fn x => cons x ys) xs) yss @ yss end

fun modes_of_term modes t =

  let

    val ks = map_index (fn (i, T) => (i + 1, NONE)) (binder_types (fastype_of t));

    val default = [Mode (([], ks), ks, [])];

    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>

        let

          val (args1, args2) =

            if length args < length iss then

              error ("Too few arguments for inductive predicate " ^ name)

            else chop (length iss) args;

          val k = length args2;

          val prfx = map (rpair NONE) (1 upto k)

        in

          if not (is_prefix op = prfx is) then [] else

          let val is' = map (fn (i, t) => (i - k, t)) (List.drop (is, k))

          in map (fn x => Mode (m, is', x)) (cprods (map

            (fn (NONE, _) => [NONE]

              | (SOME js, arg) => map SOME (filter

                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))

                    (iss ~~ args1)))

          end

        end)) (AList.lookup op = modes name)

  in

    case strip_comb (Envir.eta_contract t) of

      (Const (name, _), args) => the_default default (mk_modes name args)

    | (Var ((name, _), _), args) => the (mk_modes name args)

    | (Free (name, _), args) => the (mk_modes name args)

    | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *)

    | _ => default

  end

fun select_mode_prem thy modes vs ps =

  find_first (is_some o snd) (ps ~~ map

    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>

          let

            val (in_ts, out_ts) = split_smode is us;

            val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;

            val vTs = maps term_vTs out_ts';

            val dupTs = map snd (duplicates (op =) vTs) @

              map_filter (AList.lookup (op =) vTs) vs;

          in

            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso

            forall (is_eqT o fastype_of) in_ts' andalso

            subset (op =) (term_vs t, vs) andalso

            forall is_eqT dupTs

          end)

            (modes_of_term modes t handle Option =>

               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))

      | Negprem (us, t) => find_first (fn Mode (_, is, _) =>

            is = map (rpair NONE) (1 upto length us) andalso

            subset (op =) (terms_vs us, vs) andalso

            subset (op =) (term_vs t, vs))

            (modes_of_term modes t handle Option =>

               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))

      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))

          else NONE

      ) ps);

fun fold_prem f (Prem (args, _)) = fold f args

  | fold_prem f (Negprem (args, _)) = fold f args

  | fold_prem f (Sidecond t) = f t

fun all_subsets [] = [[]]

  | all_subsets (x::xs) = let val xss' = all_subsets xs in xss' @ (map (cons x) xss') end

fun generator vTs v = 

  let

    val T = the (AList.lookup (op =) vTs v)

  in

    (Generator (v, T), Mode (([], []), [], []))

  end;

fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =

  let

    val modes' = modes @ map_filter

      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))

        (param_vs ~~ iss);

    val gen_modes' = gen_modes @ map_filter

      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))

        (param_vs ~~ iss);  

    val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))

    val prem_vs = distinct (op =) ((fold o fold_prem) Term.add_free_names ps [])

    fun check_mode_prems acc_ps vs [] = SOME (acc_ps, vs)

      | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of

          NONE =>

            (if with_generator then

              (case select_mode_prem thy gen_modes' vs ps of

                SOME (p as Prem _, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 

                  (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)

                  (filter_out (equal p) ps)