src/HOL/Tools/Predicate_Compile/core_data.ML
author bulwahn
Thu Oct 21 19:13:09 2010 +0200 (2010-10-21)
changeset 40052 ea46574ca815
child 40053 3fa49ea76cbb
permissions -rw-r--r--
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn@40052
     1
bulwahn@40052
     2
structure Core_Data =
bulwahn@40052
     3
struct
bulwahn@40052
     4
bulwahn@40052
     5
open Predicate_Compile_Aux;
bulwahn@40052
     6
bulwahn@40052
     7
(* book-keeping *)
bulwahn@40052
     8
bulwahn@40052
     9
datatype predfun_data = PredfunData of {
bulwahn@40052
    10
  definition : thm,
bulwahn@40052
    11
  intro : thm,
bulwahn@40052
    12
  elim : thm,
bulwahn@40052
    13
  neg_intro : thm option
bulwahn@40052
    14
};
bulwahn@40052
    15
bulwahn@40052
    16
fun rep_predfun_data (PredfunData data) = data;
bulwahn@40052
    17
bulwahn@40052
    18
fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
bulwahn@40052
    19
  PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
bulwahn@40052
    20
bulwahn@40052
    21
datatype pred_data = PredData of {
bulwahn@40052
    22
  intros : (string option * thm) list,
bulwahn@40052
    23
  elim : thm option,
bulwahn@40052
    24
  preprocessed : bool,
bulwahn@40052
    25
  function_names : (compilation * (mode * string) list) list,
bulwahn@40052
    26
  predfun_data : (mode * predfun_data) list,
bulwahn@40052
    27
  needs_random : mode list
bulwahn@40052
    28
};
bulwahn@40052
    29
bulwahn@40052
    30
fun rep_pred_data (PredData data) = data;
bulwahn@40052
    31
bulwahn@40052
    32
fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
bulwahn@40052
    33
  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
bulwahn@40052
    34
    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
bulwahn@40052
    35
bulwahn@40052
    36
fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
bulwahn@40052
    37
  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
bulwahn@40052
    38
bulwahn@40052
    39
fun eq_option eq (NONE, NONE) = true
bulwahn@40052
    40
  | eq_option eq (SOME x, SOME y) = eq (x, y)
bulwahn@40052
    41
  | eq_option eq _ = false
bulwahn@40052
    42
bulwahn@40052
    43
fun eq_pred_data (PredData d1, PredData d2) = 
bulwahn@40052
    44
  eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
bulwahn@40052
    45
  eq_option Thm.eq_thm (#elim d1, #elim d2)
bulwahn@40052
    46
bulwahn@40052
    47
structure PredData = Theory_Data
bulwahn@40052
    48
(
bulwahn@40052
    49
  type T = pred_data Graph.T;
bulwahn@40052
    50
  val empty = Graph.empty;
bulwahn@40052
    51
  val extend = I;
bulwahn@40052
    52
  val merge = Graph.merge eq_pred_data;
bulwahn@40052
    53
);
bulwahn@40052
    54
bulwahn@40052
    55
(* queries *)
bulwahn@40052
    56
bulwahn@40052
    57
fun lookup_pred_data ctxt name =
bulwahn@40052
    58
  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
bulwahn@40052
    59
bulwahn@40052
    60
fun the_pred_data ctxt name = case lookup_pred_data ctxt name
bulwahn@40052
    61
 of NONE => error ("No such predicate " ^ quote name)  
bulwahn@40052
    62
  | SOME data => data;
bulwahn@40052
    63
bulwahn@40052
    64
val is_registered = is_some oo lookup_pred_data
bulwahn@40052
    65
bulwahn@40052
    66
val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
bulwahn@40052
    67
bulwahn@40052
    68
val intros_of = map snd o #intros oo the_pred_data
bulwahn@40052
    69
bulwahn@40052
    70
val names_of = map fst o #intros oo the_pred_data
bulwahn@40052
    71
bulwahn@40052
    72
fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
bulwahn@40052
    73
 of NONE => error ("No elimination rule for predicate " ^ quote name)
bulwahn@40052
    74
  | SOME thm => thm
bulwahn@40052
    75
  
bulwahn@40052
    76
val has_elim = is_some o #elim oo the_pred_data
bulwahn@40052
    77
bulwahn@40052
    78
fun function_names_of compilation ctxt name =
bulwahn@40052
    79
  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
bulwahn@40052
    80
    NONE => error ("No " ^ string_of_compilation compilation
bulwahn@40052
    81
      ^ " functions defined for predicate " ^ quote name)
bulwahn@40052
    82
  | SOME fun_names => fun_names
bulwahn@40052
    83
bulwahn@40052
    84
fun function_name_of compilation ctxt name mode =
bulwahn@40052
    85
  case AList.lookup eq_mode
bulwahn@40052
    86
    (function_names_of compilation ctxt name) mode of
bulwahn@40052
    87
    NONE => error ("No " ^ string_of_compilation compilation
bulwahn@40052
    88
      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
bulwahn@40052
    89
  | SOME function_name => function_name
bulwahn@40052
    90
bulwahn@40052
    91
fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
bulwahn@40052
    92
bulwahn@40052
    93
fun all_modes_of compilation ctxt =
bulwahn@40052
    94
  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
bulwahn@40052
    95
    (all_preds_of ctxt)
bulwahn@40052
    96
bulwahn@40052
    97
val all_random_modes_of = all_modes_of Random
bulwahn@40052
    98
bulwahn@40052
    99
fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
bulwahn@40052
   100
    NONE => false
bulwahn@40052
   101
  | SOME data => AList.defined (op =) (#function_names data) compilation
bulwahn@40052
   102
bulwahn@40052
   103
fun needs_random ctxt s m =
bulwahn@40052
   104
  member (op =) (#needs_random (the_pred_data ctxt s)) m
bulwahn@40052
   105
bulwahn@40052
   106
fun lookup_predfun_data ctxt name mode =
bulwahn@40052
   107
  Option.map rep_predfun_data
bulwahn@40052
   108
    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
bulwahn@40052
   109
bulwahn@40052
   110
fun the_predfun_data ctxt name mode =
bulwahn@40052
   111
  case lookup_predfun_data ctxt name mode of
bulwahn@40052
   112
    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
bulwahn@40052
   113
      " of predicate " ^ name)
bulwahn@40052
   114
  | SOME data => data;
bulwahn@40052
   115
bulwahn@40052
   116
val predfun_definition_of = #definition ooo the_predfun_data
bulwahn@40052
   117
bulwahn@40052
   118
val predfun_intro_of = #intro ooo the_predfun_data
bulwahn@40052
   119
bulwahn@40052
   120
val predfun_elim_of = #elim ooo the_predfun_data
bulwahn@40052
   121
bulwahn@40052
   122
val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
bulwahn@40052
   123
bulwahn@40052
   124
val intros_graph_of =
bulwahn@40052
   125
  Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
bulwahn@40052
   126
bulwahn@40052
   127
(* registration of alternative function names *)
bulwahn@40052
   128
bulwahn@40052
   129
structure Alt_Compilations_Data = Theory_Data
bulwahn@40052
   130
(
bulwahn@40052
   131
  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
bulwahn@40052
   132
  val empty = Symtab.empty;
bulwahn@40052
   133
  val extend = I;
bulwahn@40052
   134
  fun merge data : T = Symtab.merge (K true) data;
bulwahn@40052
   135
);
bulwahn@40052
   136
bulwahn@40052
   137
fun alternative_compilation_of_global thy pred_name mode =
bulwahn@40052
   138
  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
bulwahn@40052
   139
bulwahn@40052
   140
fun alternative_compilation_of ctxt pred_name mode =
bulwahn@40052
   141
  AList.lookup eq_mode
bulwahn@40052
   142
    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
bulwahn@40052
   143
bulwahn@40052
   144
fun force_modes_and_compilations pred_name compilations =
bulwahn@40052
   145
  let
bulwahn@40052
   146
    (* thm refl is a dummy thm *)
bulwahn@40052
   147
    val modes = map fst compilations
bulwahn@40052
   148
    val (needs_random, non_random_modes) = pairself (map fst)
bulwahn@40052
   149
      (List.partition (fn (m, (fun_name, random)) => random) compilations)
bulwahn@40052
   150
    val non_random_dummys = map (rpair "dummy") non_random_modes
bulwahn@40052
   151
    val all_dummys = map (rpair "dummy") modes
bulwahn@40052
   152
    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
bulwahn@40052
   153
      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
bulwahn@40052
   154
    val alt_compilations = map (apsnd fst) compilations
bulwahn@40052
   155
  in
bulwahn@40052
   156
    PredData.map (Graph.new_node
bulwahn@40052
   157
      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
bulwahn@40052
   158
    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
bulwahn@40052
   159
  end
bulwahn@40052
   160
bulwahn@40052
   161
fun functional_compilation fun_name mode compfuns T =
bulwahn@40052
   162
  let
bulwahn@40052
   163
    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
bulwahn@40052
   164
      mode (binder_types T)
bulwahn@40052
   165
    val bs = map (pair "x") inpTs
bulwahn@40052
   166
    val bounds = map Bound (rev (0 upto (length bs) - 1))
bulwahn@40052
   167
    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
bulwahn@40052
   168
  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
bulwahn@40052
   169
bulwahn@40052
   170
fun register_alternative_function pred_name mode fun_name =
bulwahn@40052
   171
  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
bulwahn@40052
   172
    (pred_name, (mode, functional_compilation fun_name mode)))
bulwahn@40052
   173
bulwahn@40052
   174
fun force_modes_and_functions pred_name fun_names =
bulwahn@40052
   175
  force_modes_and_compilations pred_name
bulwahn@40052
   176
    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
bulwahn@40052
   177
    fun_names)
bulwahn@40052
   178
bulwahn@40052
   179
end;