src/HOL/Tools/Predicate_Compile/core_data.ML
author bulwahn
Mon Oct 25 21:17:15 2010 +0200 (2010-10-25)
changeset 40140 8282b87f957c
parent 40101 f7fc517e21c6
child 41225 bd4ecd48c21f
permissions -rw-r--r--
using mode_eq instead of op = for lookup in the predicate compiler
bulwahn@40053
     1
(*  Title:      HOL/Tools/Predicate_Compile/core_data.ML
bulwahn@40053
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@40052
     3
bulwahn@40053
     4
Data of the predicate compiler core
bulwahn@40053
     5
bulwahn@40053
     6
*)
bulwahn@40053
     7
signature CORE_DATA =
bulwahn@40053
     8
sig
bulwahn@40053
     9
  type mode = Predicate_Compile_Aux.mode
bulwahn@40053
    10
  type compilation = Predicate_Compile_Aux.compilation
bulwahn@40053
    11
  type compilation_funs = Predicate_Compile_Aux.compilation_funs
bulwahn@40053
    12
  
bulwahn@40053
    13
  datatype predfun_data = PredfunData of {
bulwahn@40053
    14
    definition : thm,
bulwahn@40053
    15
    intro : thm,
bulwahn@40053
    16
    elim : thm,
bulwahn@40053
    17
    neg_intro : thm option
bulwahn@40053
    18
  };
bulwahn@40053
    19
bulwahn@40053
    20
  datatype pred_data = PredData of {
bulwahn@40053
    21
    intros : (string option * thm) list,
bulwahn@40053
    22
    elim : thm option,
bulwahn@40053
    23
    preprocessed : bool,
bulwahn@40053
    24
    function_names : (compilation * (mode * string) list) list,
bulwahn@40053
    25
    predfun_data : (mode * predfun_data) list,
bulwahn@40053
    26
    needs_random : mode list
bulwahn@40053
    27
  };
bulwahn@40053
    28
bulwahn@40053
    29
  structure PredData : THEORY_DATA
bulwahn@40053
    30
  
bulwahn@40053
    31
  (* queries *)
bulwahn@40053
    32
  val defined_functions : compilation -> Proof.context -> string -> bool
bulwahn@40053
    33
  val is_registered : Proof.context -> string -> bool
bulwahn@40053
    34
  val function_name_of : compilation -> Proof.context -> string -> mode -> string
bulwahn@40053
    35
  val the_elim_of : Proof.context -> string -> thm
bulwahn@40053
    36
  val has_elim : Proof.context -> string -> bool
bulwahn@40053
    37
  
bulwahn@40053
    38
  val needs_random : Proof.context -> string -> mode -> bool
bulwahn@40053
    39
  
bulwahn@40053
    40
  val predfun_intro_of : Proof.context -> string -> mode -> thm
bulwahn@40053
    41
  val predfun_neg_intro_of : Proof.context -> string -> mode -> thm option
bulwahn@40053
    42
  val predfun_elim_of : Proof.context -> string -> mode -> thm
bulwahn@40053
    43
  val predfun_definition_of : Proof.context -> string -> mode -> thm
bulwahn@40053
    44
  
bulwahn@40053
    45
  val all_preds_of : Proof.context -> string list
bulwahn@40053
    46
  val modes_of: compilation -> Proof.context -> string -> mode list
bulwahn@40053
    47
  val all_modes_of : compilation -> Proof.context -> (string * mode list) list
bulwahn@40053
    48
  val all_random_modes_of : Proof.context -> (string * mode list) list
bulwahn@40053
    49
  val intros_of : Proof.context -> string -> thm list
bulwahn@40053
    50
  val names_of : Proof.context -> string -> string option list
bulwahn@40053
    51
bulwahn@40053
    52
  val intros_graph_of : Proof.context -> thm list Graph.T
bulwahn@40053
    53
  
bulwahn@40053
    54
  (* updaters *)
bulwahn@40053
    55
  
bulwahn@40053
    56
  val register_predicate : (string * thm list * thm) -> theory -> theory
bulwahn@40053
    57
  val register_intros : string * thm list -> theory -> theory
bulwahn@40053
    58
bulwahn@40053
    59
  (* FIXME: naming of function is strange *)
bulwahn@40053
    60
  val defined_function_of : compilation -> string -> theory -> theory
bulwahn@40053
    61
  val add_intro : string option * thm -> theory -> theory
bulwahn@40053
    62
  val set_elim : thm -> theory -> theory
bulwahn@40053
    63
  val set_function_name : compilation -> string -> mode -> string -> theory -> theory
bulwahn@40053
    64
  val add_predfun_data : string -> mode -> thm * ((thm * thm) * thm option) -> theory -> theory
bulwahn@40053
    65
  val set_needs_random : string -> mode list -> theory -> theory
bulwahn@40053
    66
  (* sophisticated updaters *)
bulwahn@40053
    67
  val extend_intro_graph : string list -> theory -> theory
bulwahn@40053
    68
  val preprocess_intros : string -> theory -> theory
bulwahn@40053
    69
  
bulwahn@40053
    70
  (* alternative function definitions *)
bulwahn@40053
    71
  val register_alternative_function : string -> mode -> string -> theory -> theory
bulwahn@40053
    72
  val alternative_compilation_of_global : theory -> string -> mode ->
bulwahn@40053
    73
    (compilation_funs -> typ -> term) option
bulwahn@40053
    74
  val alternative_compilation_of : Proof.context -> string -> mode ->
bulwahn@40053
    75
    (compilation_funs -> typ -> term) option
bulwahn@40053
    76
  val functional_compilation : string -> mode -> compilation_funs -> typ -> term
bulwahn@40053
    77
  val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
bulwahn@40053
    78
  val force_modes_and_compilations : string ->
bulwahn@40053
    79
    (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
bulwahn@40053
    80
bulwahn@40053
    81
end;
bulwahn@40053
    82
bulwahn@40053
    83
structure Core_Data : CORE_DATA =
bulwahn@40052
    84
struct
bulwahn@40052
    85
bulwahn@40052
    86
open Predicate_Compile_Aux;
bulwahn@40052
    87
bulwahn@40052
    88
(* book-keeping *)
bulwahn@40052
    89
bulwahn@40052
    90
datatype predfun_data = PredfunData of {
bulwahn@40052
    91
  definition : thm,
bulwahn@40052
    92
  intro : thm,
bulwahn@40052
    93
  elim : thm,
bulwahn@40052
    94
  neg_intro : thm option
bulwahn@40052
    95
};
bulwahn@40052
    96
bulwahn@40052
    97
fun rep_predfun_data (PredfunData data) = data;
bulwahn@40052
    98
bulwahn@40052
    99
fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
bulwahn@40052
   100
  PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
bulwahn@40052
   101
bulwahn@40052
   102
datatype pred_data = PredData of {
bulwahn@40052
   103
  intros : (string option * thm) list,
bulwahn@40052
   104
  elim : thm option,
bulwahn@40052
   105
  preprocessed : bool,
bulwahn@40052
   106
  function_names : (compilation * (mode * string) list) list,
bulwahn@40052
   107
  predfun_data : (mode * predfun_data) list,
bulwahn@40052
   108
  needs_random : mode list
bulwahn@40052
   109
};
bulwahn@40052
   110
bulwahn@40052
   111
fun rep_pred_data (PredData data) = data;
bulwahn@40052
   112
bulwahn@40052
   113
fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
bulwahn@40052
   114
  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
bulwahn@40052
   115
    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
bulwahn@40052
   116
bulwahn@40052
   117
fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
bulwahn@40052
   118
  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
bulwahn@40052
   119
bulwahn@40052
   120
fun eq_option eq (NONE, NONE) = true
bulwahn@40052
   121
  | eq_option eq (SOME x, SOME y) = eq (x, y)
bulwahn@40052
   122
  | eq_option eq _ = false
bulwahn@40052
   123
bulwahn@40052
   124
fun eq_pred_data (PredData d1, PredData d2) = 
bulwahn@40052
   125
  eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
bulwahn@40052
   126
  eq_option Thm.eq_thm (#elim d1, #elim d2)
bulwahn@40052
   127
bulwahn@40052
   128
structure PredData = Theory_Data
bulwahn@40052
   129
(
bulwahn@40052
   130
  type T = pred_data Graph.T;
bulwahn@40052
   131
  val empty = Graph.empty;
bulwahn@40052
   132
  val extend = I;
bulwahn@40052
   133
  val merge = Graph.merge eq_pred_data;
bulwahn@40052
   134
);
bulwahn@40052
   135
bulwahn@40052
   136
(* queries *)
bulwahn@40052
   137
bulwahn@40052
   138
fun lookup_pred_data ctxt name =
bulwahn@40052
   139
  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
bulwahn@40052
   140
bulwahn@40052
   141
fun the_pred_data ctxt name = case lookup_pred_data ctxt name
bulwahn@40052
   142
 of NONE => error ("No such predicate " ^ quote name)  
bulwahn@40052
   143
  | SOME data => data;
bulwahn@40052
   144
bulwahn@40052
   145
val is_registered = is_some oo lookup_pred_data
bulwahn@40052
   146
bulwahn@40052
   147
val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
bulwahn@40052
   148
bulwahn@40052
   149
val intros_of = map snd o #intros oo the_pred_data
bulwahn@40052
   150
bulwahn@40052
   151
val names_of = map fst o #intros oo the_pred_data
bulwahn@40052
   152
bulwahn@40052
   153
fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
bulwahn@40052
   154
 of NONE => error ("No elimination rule for predicate " ^ quote name)
bulwahn@40052
   155
  | SOME thm => thm
bulwahn@40052
   156
  
bulwahn@40052
   157
val has_elim = is_some o #elim oo the_pred_data
bulwahn@40052
   158
bulwahn@40052
   159
fun function_names_of compilation ctxt name =
bulwahn@40052
   160
  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
bulwahn@40052
   161
    NONE => error ("No " ^ string_of_compilation compilation
bulwahn@40052
   162
      ^ " functions defined for predicate " ^ quote name)
bulwahn@40052
   163
  | SOME fun_names => fun_names
bulwahn@40052
   164
bulwahn@40052
   165
fun function_name_of compilation ctxt name mode =
bulwahn@40052
   166
  case AList.lookup eq_mode
bulwahn@40052
   167
    (function_names_of compilation ctxt name) mode of
bulwahn@40052
   168
    NONE => error ("No " ^ string_of_compilation compilation
bulwahn@40052
   169
      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
bulwahn@40052
   170
  | SOME function_name => function_name
bulwahn@40052
   171
bulwahn@40052
   172
fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
bulwahn@40052
   173
bulwahn@40052
   174
fun all_modes_of compilation ctxt =
bulwahn@40052
   175
  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
bulwahn@40052
   176
    (all_preds_of ctxt)
bulwahn@40052
   177
bulwahn@40052
   178
val all_random_modes_of = all_modes_of Random
bulwahn@40052
   179
bulwahn@40052
   180
fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
bulwahn@40052
   181
    NONE => false
bulwahn@40052
   182
  | SOME data => AList.defined (op =) (#function_names data) compilation
bulwahn@40052
   183
bulwahn@40052
   184
fun needs_random ctxt s m =
bulwahn@40052
   185
  member (op =) (#needs_random (the_pred_data ctxt s)) m
bulwahn@40052
   186
bulwahn@40052
   187
fun lookup_predfun_data ctxt name mode =
bulwahn@40052
   188
  Option.map rep_predfun_data
bulwahn@40140
   189
    (AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
bulwahn@40052
   190
bulwahn@40052
   191
fun the_predfun_data ctxt name mode =
bulwahn@40052
   192
  case lookup_predfun_data ctxt name mode of
bulwahn@40052
   193
    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
bulwahn@40052
   194
      " of predicate " ^ name)
bulwahn@40052
   195
  | SOME data => data;
bulwahn@40052
   196
bulwahn@40052
   197
val predfun_definition_of = #definition ooo the_predfun_data
bulwahn@40052
   198
bulwahn@40052
   199
val predfun_intro_of = #intro ooo the_predfun_data
bulwahn@40052
   200
bulwahn@40052
   201
val predfun_elim_of = #elim ooo the_predfun_data
bulwahn@40052
   202
bulwahn@40052
   203
val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
bulwahn@40052
   204
bulwahn@40052
   205
val intros_graph_of =
bulwahn@40052
   206
  Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
bulwahn@40052
   207
bulwahn@40053
   208
fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
bulwahn@40053
   209
  let
bulwahn@40053
   210
    val thy = ProofContext.theory_of ctxt
bulwahn@40053
   211
    val nargs = length (binder_types (fastype_of pred))
bulwahn@40053
   212
    fun PEEK f dependent_tactic st = dependent_tactic (f st) st
bulwahn@40053
   213
    fun meta_eq_of th = th RS @{thm eq_reflection}
bulwahn@40053
   214
    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
bulwahn@40053
   215
    fun instantiate i n {context = ctxt, params = p, prems = prems,
bulwahn@40053
   216
      asms = a, concl = cl, schematics = s}  =
bulwahn@40053
   217
      let
bulwahn@40053
   218
        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
bulwahn@40053
   219
        fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
bulwahn@40053
   220
          |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
bulwahn@40053
   221
        val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
bulwahn@40053
   222
        val case_th = MetaSimplifier.simplify true
bulwahn@40053
   223
          (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
bulwahn@40053
   224
        val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
bulwahn@40053
   225
        val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
bulwahn@40053
   226
        val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
bulwahn@40053
   227
          OF (replicate nargs @{thm refl})
bulwahn@40053
   228
        val thesis =
bulwahn@40053
   229
          Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
bulwahn@40053
   230
            OF prems'
bulwahn@40053
   231
      in
bulwahn@40053
   232
        (rtac thesis 1)
bulwahn@40053
   233
      end
bulwahn@40053
   234
    val tac =
bulwahn@40053
   235
      etac pre_cases_rule 1
bulwahn@40053
   236
      THEN
bulwahn@40053
   237
      (PEEK nprems_of
bulwahn@40053
   238
        (fn n =>
bulwahn@40053
   239
          ALLGOALS (fn i =>
bulwahn@40053
   240
            MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
bulwahn@40053
   241
            THEN (SUBPROOF (instantiate i n) ctxt i))))
bulwahn@40053
   242
  in
bulwahn@40053
   243
    Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
bulwahn@40053
   244
  end
bulwahn@40053
   245
bulwahn@40053
   246
(* updaters *)
bulwahn@40053
   247
bulwahn@40053
   248
(* fetching introduction rules or registering introduction rules *)
bulwahn@40053
   249
bulwahn@40053
   250
val no_compilation = ([], ([], []))
bulwahn@40053
   251
bulwahn@40053
   252
fun fetch_pred_data ctxt name =
bulwahn@40053
   253
  case try (Inductive.the_inductive ctxt) name of
bulwahn@40053
   254
    SOME (info as (_, result)) => 
bulwahn@40053
   255
      let
bulwahn@40053
   256
        fun is_intro_of intro =
bulwahn@40053
   257
          let
bulwahn@40053
   258
            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
bulwahn@40053
   259
          in (fst (dest_Const const) = name) end;
bulwahn@40053
   260
        val thy = ProofContext.theory_of ctxt
bulwahn@40053
   261
        val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
bulwahn@40053
   262
        val index = find_index (fn s => s = name) (#names (fst info))
bulwahn@40053
   263
        val pre_elim = nth (#elims result) index
bulwahn@40053
   264
        val pred = nth (#preds result) index
bulwahn@40053
   265
        val elim_t = mk_casesrule ctxt pred intros
bulwahn@40053
   266
        val nparams = length (Inductive.params_of (#raw_induct result))
bulwahn@40053
   267
        val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
bulwahn@40053
   268
      in
bulwahn@40053
   269
        mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
bulwahn@40053
   270
      end
bulwahn@40053
   271
  | NONE => error ("No such predicate: " ^ quote name)
bulwahn@40053
   272
bulwahn@40053
   273
fun add_predfun_data name mode data =
bulwahn@40053
   274
  let
bulwahn@40053
   275
    val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
bulwahn@40053
   276
  in PredData.map (Graph.map_node name (map_pred_data add)) end
bulwahn@40053
   277
bulwahn@40053
   278
fun is_inductive_predicate ctxt name =
bulwahn@40053
   279
  is_some (try (Inductive.the_inductive ctxt) name)
bulwahn@40053
   280
bulwahn@40053
   281
fun depending_preds_of ctxt (key, value) =
bulwahn@40053
   282
  let
bulwahn@40053
   283
    val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
bulwahn@40053
   284
  in
bulwahn@40053
   285
    fold Term.add_const_names intros []
bulwahn@40053
   286
      |> (fn cs =>
bulwahn@40053
   287
        if member (op =) cs @{const_name "HOL.eq"} then
bulwahn@40053
   288
          insert (op =) @{const_name Predicate.eq} cs
bulwahn@40053
   289
        else cs)
bulwahn@40053
   290
      |> filter (fn c => (not (c = key)) andalso
bulwahn@40053
   291
        (is_inductive_predicate ctxt c orelse is_registered ctxt c))
bulwahn@40053
   292
  end;
bulwahn@40053
   293
bulwahn@40053
   294
fun add_intro (opt_case_name, thm) thy =
bulwahn@40053
   295
  let
bulwahn@40053
   296
    val (name, T) = dest_Const (fst (strip_intro_concl thm))
bulwahn@40053
   297
    fun cons_intro gr =
bulwahn@40053
   298
     case try (Graph.get_node gr) name of
bulwahn@40053
   299
       SOME pred_data => Graph.map_node name (map_pred_data
bulwahn@40053
   300
         (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
bulwahn@40053
   301
     | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
bulwahn@40053
   302
  in PredData.map cons_intro thy end
bulwahn@40053
   303
bulwahn@40053
   304
fun set_elim thm =
bulwahn@40053
   305
  let
bulwahn@40053
   306
    val (name, _) = dest_Const (fst 
bulwahn@40053
   307
      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
bulwahn@40053
   308
  in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
bulwahn@40053
   309
bulwahn@40053
   310
fun register_predicate (constname, intros, elim) thy =
bulwahn@40053
   311
  let
bulwahn@40053
   312
    val named_intros = map (pair NONE) intros
bulwahn@40053
   313
  in
bulwahn@40053
   314
    if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
bulwahn@40053
   315
      PredData.map
bulwahn@40053
   316
        (Graph.new_node (constname,
bulwahn@40053
   317
          mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
bulwahn@40053
   318
    else thy
bulwahn@40053
   319
  end
bulwahn@40053
   320
bulwahn@40053
   321
fun register_intros (constname, pre_intros) thy =
bulwahn@40053
   322
  let
bulwahn@40053
   323
    val T = Sign.the_const_type thy constname
bulwahn@40053
   324
    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
bulwahn@40053
   325
    val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
bulwahn@40053
   326
      error ("register_intros: Introduction rules of different constants are used\n" ^
bulwahn@40053
   327
        "expected rules for " ^ constname ^ ", but received rules for " ^
bulwahn@40053
   328
          commas (map constname_of_intro pre_intros))
bulwahn@40053
   329
      else ()
bulwahn@40053
   330
    val pred = Const (constname, T)
bulwahn@40053
   331
    val pre_elim = 
bulwahn@40053
   332
      (Drule.export_without_context o Skip_Proof.make_thm thy)
bulwahn@40053
   333
      (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
bulwahn@40053
   334
  in register_predicate (constname, pre_intros, pre_elim) thy end
bulwahn@40053
   335
bulwahn@40053
   336
fun defined_function_of compilation pred =
bulwahn@40053
   337
  let
bulwahn@40053
   338
    val set = (apsnd o apfst) (cons (compilation, []))
bulwahn@40053
   339
  in
bulwahn@40053
   340
    PredData.map (Graph.map_node pred (map_pred_data set))
bulwahn@40053
   341
  end
bulwahn@40053
   342
bulwahn@40053
   343
fun set_function_name compilation pred mode name =
bulwahn@40053
   344
  let
bulwahn@40053
   345
    val set = (apsnd o apfst)
bulwahn@40053
   346
      (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
bulwahn@40053
   347
  in
bulwahn@40053
   348
    PredData.map (Graph.map_node pred (map_pred_data set))
bulwahn@40053
   349
  end
bulwahn@40053
   350
bulwahn@40053
   351
fun set_needs_random name modes =
bulwahn@40053
   352
  let
bulwahn@40053
   353
    val set = (apsnd o apsnd o apsnd) (K modes)
bulwahn@40053
   354
  in
bulwahn@40053
   355
    PredData.map (Graph.map_node name (map_pred_data set))
bulwahn@40053
   356
  end  
bulwahn@40053
   357
bulwahn@40053
   358
fun extend' value_of edges_of key (G, visited) =
bulwahn@40053
   359
  let
bulwahn@40053
   360
    val (G', v) = case try (Graph.get_node G) key of
bulwahn@40053
   361
        SOME v => (G, v)
bulwahn@40053
   362
      | NONE => (Graph.new_node (key, value_of key) G, value_of key)
bulwahn@40053
   363
    val (G'', visited') = fold (extend' value_of edges_of)
bulwahn@40053
   364
      (subtract (op =) visited (edges_of (key, v)))
bulwahn@40053
   365
      (G', key :: visited)
bulwahn@40053
   366
  in
bulwahn@40053
   367
    (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
bulwahn@40053
   368
  end;
bulwahn@40053
   369
bulwahn@40053
   370
fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
bulwahn@40053
   371
bulwahn@40053
   372
fun extend_intro_graph names thy =
bulwahn@40053
   373
  let
bulwahn@40053
   374
    val ctxt = ProofContext.init_global thy
bulwahn@40053
   375
  in
bulwahn@40053
   376
    PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) thy
bulwahn@40053
   377
  end
bulwahn@40053
   378
bulwahn@40053
   379
fun preprocess_intros name thy =
bulwahn@40053
   380
  PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
bulwahn@40053
   381
    if preprocessed then (rules, preprocessed)
bulwahn@40053
   382
    else
bulwahn@40053
   383
      let
bulwahn@40053
   384
        val (named_intros, SOME elim) = rules
bulwahn@40053
   385
        val named_intros' = map (apsnd (preprocess_intro thy)) named_intros
bulwahn@40053
   386
        val pred = Const (name, Sign.the_const_type thy name)
bulwahn@40053
   387
        val ctxt = ProofContext.init_global thy
bulwahn@40053
   388
        val elim_t = mk_casesrule ctxt pred (map snd named_intros')
bulwahn@40053
   389
        val nparams = (case try (Inductive.the_inductive ctxt) name of
bulwahn@40053
   390
            SOME (_, result) => length (Inductive.params_of (#raw_induct result))
bulwahn@40053
   391
          | NONE => 0)
bulwahn@40053
   392
        val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
bulwahn@40053
   393
      in
bulwahn@40053
   394
        ((named_intros', SOME elim'), true)
bulwahn@40053
   395
      end))))
bulwahn@40053
   396
    thy  
bulwahn@40053
   397
bulwahn@40052
   398
(* registration of alternative function names *)
bulwahn@40052
   399
bulwahn@40052
   400
structure Alt_Compilations_Data = Theory_Data
bulwahn@40052
   401
(
bulwahn@40052
   402
  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
bulwahn@40052
   403
  val empty = Symtab.empty;
bulwahn@40052
   404
  val extend = I;
bulwahn@40052
   405
  fun merge data : T = Symtab.merge (K true) data;
bulwahn@40052
   406
);
bulwahn@40052
   407
bulwahn@40052
   408
fun alternative_compilation_of_global thy pred_name mode =
bulwahn@40052
   409
  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
bulwahn@40052
   410
bulwahn@40052
   411
fun alternative_compilation_of ctxt pred_name mode =
bulwahn@40052
   412
  AList.lookup eq_mode
bulwahn@40052
   413
    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
bulwahn@40052
   414
bulwahn@40052
   415
fun force_modes_and_compilations pred_name compilations =
bulwahn@40052
   416
  let
bulwahn@40052
   417
    (* thm refl is a dummy thm *)
bulwahn@40052
   418
    val modes = map fst compilations
bulwahn@40052
   419
    val (needs_random, non_random_modes) = pairself (map fst)
bulwahn@40052
   420
      (List.partition (fn (m, (fun_name, random)) => random) compilations)
bulwahn@40052
   421
    val non_random_dummys = map (rpair "dummy") non_random_modes
bulwahn@40052
   422
    val all_dummys = map (rpair "dummy") modes
bulwahn@40052
   423
    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
bulwahn@40052
   424
      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
bulwahn@40052
   425
    val alt_compilations = map (apsnd fst) compilations
bulwahn@40052
   426
  in
bulwahn@40052
   427
    PredData.map (Graph.new_node
bulwahn@40052
   428
      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
bulwahn@40052
   429
    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
bulwahn@40052
   430
  end
bulwahn@40052
   431
bulwahn@40052
   432
fun functional_compilation fun_name mode compfuns T =
bulwahn@40052
   433
  let
bulwahn@40052
   434
    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
bulwahn@40052
   435
      mode (binder_types T)
bulwahn@40052
   436
    val bs = map (pair "x") inpTs
bulwahn@40052
   437
    val bounds = map Bound (rev (0 upto (length bs) - 1))
bulwahn@40052
   438
    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
bulwahn@40052
   439
  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
bulwahn@40052
   440
bulwahn@40052
   441
fun register_alternative_function pred_name mode fun_name =
bulwahn@40052
   442
  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
bulwahn@40052
   443
    (pred_name, (mode, functional_compilation fun_name mode)))
bulwahn@40052
   444
bulwahn@40052
   445
fun force_modes_and_functions pred_name fun_names =
bulwahn@40052
   446
  force_modes_and_compilations pred_name
bulwahn@40052
   447
    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
bulwahn@40052
   448
    fun_names)
bulwahn@40052
   449
bulwahn@40052
   450
end;