(* Author: Lukas Bulwahn, TU Muenchen

(Prototype of) 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

  type smode = (int * int list option) list

  type mode = smode option list * smode

  datatype tmode = Mode of mode * smode * tmode option list;

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

  val register_intros : thm list -> theory -> theory

  val is_registered : theory -> string -> bool

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

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

    (*  val strip_intro_concl: int -> term -> term * (term list * term list)*)

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

  val all_preds_of : theory -> string list

  val modes_of: theory -> string -> mode list

  val depth_limited_modes_of: theory -> string -> mode list

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

  val generator_modes_of: theory -> string -> mode list

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

  val string_of_mode : mode -> string

  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 do_proofs: bool Unsynchronized.ref

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

    (*  val analyze_compr: theory -> compfuns -> int option * bool -> term -> 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 add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory

  val code_pred_intros_attrib : attribute

  (* used by Quickcheck_Generator *) 

  (* temporary for testing of the compilation *)

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

    GeneratorPrem of term list * term | Generator of (string * typ);

  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,

    lift_pred : term -> term

  };  

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

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

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

    -> (string * mode list) list

    -> string list

    -> (string * (term list * indprem list) list) list

    -> (moded_clause list) pred_mode_table

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

    -> (string * mode list) list

    -> string list

    -> (string * (term list * indprem list) list) list

    -> (moded_clause list) pred_mode_table  

  (*val compile_preds : theory -> compilation_funs -> string list -> string list

    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table

  val rpred_create_definitions :(string * typ) list -> string * mode list

    -> theory -> theory 

  val split_smode : int list -> term list -> (term list * term list) *)

  val print_moded_clauses :

    theory -> (moded_clause list) pred_mode_table -> unit

  val print_compiled_terms : theory -> term pred_mode_table -> unit

  (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*)

  val pred_compfuns : compilation_funs

  val rpred_compfuns : compilation_funs

  val dest_funT : typ -> typ * typ

 (* val depending_preds_of : theory -> thm list -> string list *)

  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

  val is_inductive_predicate : theory -> string -> bool

  val terms_vs : term list -> string list

  val subsets : int -> int -> int list list

  val check_mode_clause : bool -> theory -> string list ->

    (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list)

      -> (term list * (indprem * tmode) list) option

  val string_of_moded_prem : theory -> (indprem * tmode) -> string

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

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

  val preprocess_intro : theory -> thm -> thm

  val is_constrt : theory -> term -> bool

  val is_predT : typ -> bool

  val guess_nparams : typ -> int

  val cprods_subset : 'a list list -> 'a list list

  val dest_prem : theory -> term list ->  term -> indprem

end;

structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =

struct

open Predicate_Compile_Aux;

(** auxiliary **)

(* debug stuff *)

fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());

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)); *)

val do_proofs = Unsynchronized.ref true;

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_tupleT [] = HOLogic.unitT

  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;

fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []

  | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)

  | dest_tupleT t = [t]

fun mk_tuple [] = HOLogic.unit

  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;

fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []

  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)

  | dest_tuple t = [t]

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 * 

*)

type smode = (int * int list option) list

type mode = smode option list * smode;

datatype tmode = Mode of mode * smode * tmode option list;

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

val split_smode = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple)   

val split_smodeT = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT)

fun gen_split_mode split_smode (iss, is) ts =

  let

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

  in (t1, split_smode is t2) end

val split_mode = gen_split_mode split_smode

val split_modeT = gen_split_mode split_smodeT

fun string_of_smode js =

    commas (map

      (fn (i, is) =>

        string_of_int i ^ (case is of NONE => ""

    | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js)

fun string_of_mode (iss, is) = space_implode " -> " (map

  (fn NONE => "X"

    | SOME js => enclose "[" "]" (string_of_smode js))

       (iss @ [SOME is]));

fun string_of_tmode (Mode (predmode, termmode, param_modes)) =

  "predmode: " ^ (string_of_mode predmode) ^ 

  (if null param_modes then "" else

    "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))

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

  GeneratorPrem of term list * 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 rpred_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

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

(* diagnostic display functions *)

fun print_modes modes =

  tracing ("Inferred modes:\n" ^

    cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map

      string_of_mode ms)) modes));

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 (GeneratorPrem (ts, p), Mode (predmode, is, _)) =

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

    "(generator_mode: " ^ (string_of_mode predmode) ^ ")"

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

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

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 (map (map (rpair NONE)) ms, map snd modes)) then

          error ("expected modes were not inferred:"

            ^ "infered modes for " ^ s ^ ": " ^ commas (map (string_of_smode o snd) modes))

        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') = foldr varify (~1, []) cs;

     val (i', intr_ts') = 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 (List.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 _ [] ctxt = ([], ctxt)

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

          val subst = Sign.typ_match thy

            (fastype_of pred', fastype_of pred) Vartab.empty

          val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T))

            (Vartab.dest subst)

        in Thm.certify_instantiate (subst', []) 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 ((_, ths'), ctxt1) =

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

    in

      (th' :: ths', ctxt1)

    end

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

fun mk_casesrule ctxt nparams introrules =

  let

    val (intros_th, ctxt1) = import_intros nparams introrules ctxt

    val intros = map prop_of intros_th

    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)

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

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

    val (argnames, ctxt3) = Variable.variant_fixes

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

    val argvs = map2 (curry Free) argnames (map fastype_of args)

    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 _ => setmp quick_and_dirty true (SkipProof.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 pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))

        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 (setmp quick_and_dirty true (SkipProof.make_thm thy)))

          (mk_casesrule (ProofContext.init thy) 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 (curry Int.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) => (thm::intros, 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 (pre_intros, pre_elim, nparams) thy =

  let

    val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd pre_intros))))

    (* 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)) name) then

      PredData.map

        (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy

    else thy

  end

fun register_intros pre_intros thy =

  let

    val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))

    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 = c) pre_intros) then

      error "register_intros: Introduction rules of different constants are used" else ()

    val nparams = guess_nparams T

    val pre_elim = 

      (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))

      (mk_casesrule (ProofContext.init thy) nparams pre_intros)

  in register_predicate (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

(** data structures for generic compilation for different monads **)

(* maybe rename functions more generic:

  mk_predT -> mk_monadT; dest_predT -> dest_monadT

  mk_single -> mk_return (?)

*)

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,

(*  funT_of : mode -> typ -> typ, *)

(*  mk_fun_of : theory -> (string * typ) -> mode -> term, *) 

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

  lift_pred : 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 funT_of (CompilationFuns funs) = #funT_of funs*)

(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)

fun mk_map (CompilationFuns funs) = #mk_map funs

fun lift_pred (CompilationFuns funs) = #lift_pred 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 (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 lift_pred = I

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, lift_pred = lift_pred};

end;

structure RPredCompFuns =

struct

fun mk_rpredT T =

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

fun dest_rpredT (Type ("fun", [_,

  Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T

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

fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)

fun mk_single t =

  let

    val T = fastype_of t

  in

    Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t

  end;

fun mk_bind (x, f) =

  let

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

  in

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

  end

val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}

fun mk_if cond = Const (@{const_name RPred.if_rpred},

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

fun mk_not t = error "Negation is not defined for RPred"

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

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

fun lift_pred t =

  let

    val T = PredicateCompFuns.dest_predT (fastype_of t)

    val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T 

  in

    Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t  

  end;

val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, 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, lift_pred = lift_pred};

end;

(* for external use with interactive mode *)

val pred_compfuns = PredicateCompFuns.compfuns

val rpred_compfuns = RPredCompFuns.compfuns;

fun lift_random random =

  let

    val T = dest_randomT (fastype_of random)

  in

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

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

      RPredCompFuns.mk_rpredT 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 PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 

  in

    (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}]) ---> (mk_predT compfuns (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 [];

(*FIXME this function should not be named merge... make it local instead*)

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;

fun subsets i j = if i <= j then

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

(*TODO: cleanup function and put together with modes_of_term *)

(*

fun modes_of_param default modes t = let

    val (vs, t') = strip_abs t

    val b = length vs