src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25 ago)
changeset 47108 2a1953f0d20d
parent 44338 700008399ee5
child 49561 26fc70e983c2
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
wenzelm@33265
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_data.ML
wenzelm@33265
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@33250
     3
wenzelm@33265
     4
Book-keeping datastructure for the predicate compiler.
wenzelm@33265
     5
*)
bulwahn@33250
     6
bulwahn@33250
     7
signature PREDICATE_COMPILE_DATA =
bulwahn@33250
     8
sig
bulwahn@35324
     9
  val ignore_consts : string list -> theory -> theory
bulwahn@35324
    10
  val keep_functions : string list -> theory -> theory
bulwahn@35324
    11
  val keep_function : theory -> string -> bool
bulwahn@35324
    12
  val processed_specs : theory -> string -> (string * thm list) list option
bulwahn@35324
    13
  val store_processed_specs : (string * (string * thm list) list) -> theory -> theory
bulwahn@35324
    14
  
bulwahn@35324
    15
  val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
bulwahn@34948
    16
  val obtain_specification_graph :
wenzelm@35404
    17
    Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
bulwahn@35324
    18
    
wenzelm@35404
    19
  val present_graph : thm list Term_Graph.T -> unit
bulwahn@33250
    20
  val normalize_equation : theory -> thm -> thm
bulwahn@33250
    21
end;
bulwahn@33250
    22
bulwahn@33250
    23
structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
bulwahn@33250
    24
struct
bulwahn@33250
    25
bulwahn@33250
    26
open Predicate_Compile_Aux;
bulwahn@33250
    27
wenzelm@33522
    28
structure Data = Theory_Data
bulwahn@33250
    29
(
bulwahn@33250
    30
  type T =
bulwahn@35324
    31
    {ignore_consts : unit Symtab.table,
bulwahn@35324
    32
     keep_functions : unit Symtab.table,
bulwahn@35324
    33
     processed_specs : ((string * thm list) list) Symtab.table};
bulwahn@33250
    34
  val empty =
bulwahn@35324
    35
    {ignore_consts = Symtab.empty,
bulwahn@35324
    36
     keep_functions = Symtab.empty,
bulwahn@35324
    37
     processed_specs =  Symtab.empty};
bulwahn@33250
    38
  val extend = I;
wenzelm@33522
    39
  fun merge
bulwahn@35324
    40
    ({ignore_consts = c1, keep_functions = k1, processed_specs = s1},
bulwahn@35324
    41
     {ignore_consts = c2, keep_functions = k2, processed_specs = s2}) =
bulwahn@35324
    42
     {ignore_consts = Symtab.merge (K true) (c1, c2),
bulwahn@35324
    43
      keep_functions = Symtab.merge (K true) (k1, k2),
bulwahn@35324
    44
      processed_specs = Symtab.merge (K true) (s1, s2)}
bulwahn@33250
    45
);
bulwahn@33250
    46
bulwahn@35324
    47
bulwahn@35324
    48
bulwahn@35324
    49
fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s}
bulwahn@35324
    50
fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
bulwahn@35324
    51
bulwahn@35324
    52
fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
bulwahn@35324
    53
bulwahn@35324
    54
fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
bulwahn@33250
    55
bulwahn@35324
    56
fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
bulwahn@35324
    57
bulwahn@35324
    58
fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
bulwahn@35324
    59
bulwahn@35324
    60
fun store_processed_specs (constname, specs) =
bulwahn@35324
    61
  Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs))))
bulwahn@35324
    62
(* *)
bulwahn@35324
    63
bulwahn@33250
    64
bulwahn@34948
    65
fun defining_term_of_introrule_term t =
bulwahn@33250
    66
  let
bulwahn@33250
    67
    val _ $ u = Logic.strip_imp_concl t
bulwahn@34948
    68
  in fst (strip_comb u) end
bulwahn@34948
    69
(*  
bulwahn@33250
    70
  in case pred of
bulwahn@33250
    71
    Const (c, T) => c
bulwahn@33250
    72
    | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
bulwahn@33250
    73
  end
bulwahn@34948
    74
*)
bulwahn@34948
    75
val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
bulwahn@33250
    76
bulwahn@40142
    77
fun defining_const_of_introrule th =
bulwahn@40142
    78
  case defining_term_of_introrule th
bulwahn@40142
    79
   of Const (c, _) => c
bulwahn@40142
    80
    | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
bulwahn@40142
    81
bulwahn@33250
    82
(*TODO*)
bulwahn@33250
    83
fun is_introlike_term t = true
bulwahn@33250
    84
bulwahn@33250
    85
val is_introlike = is_introlike_term o prop_of
bulwahn@33250
    86
bulwahn@33250
    87
fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
bulwahn@33250
    88
  (case strip_comb u of
bulwahn@33250
    89
    (Const (c, T), args) =>
bulwahn@33250
    90
      if (length (binder_types T) = length args) then
bulwahn@33250
    91
        true
bulwahn@33250
    92
      else
bulwahn@33250
    93
        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
bulwahn@33250
    94
  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
bulwahn@33250
    95
  | check_equation_format_term t =
bulwahn@33250
    96
    raise TERM ("check_equation_format_term failed: Not an equation", [t])
bulwahn@33250
    97
bulwahn@33250
    98
val check_equation_format = check_equation_format_term o prop_of
bulwahn@33250
    99
bulwahn@34948
   100
bulwahn@34948
   101
fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u)
bulwahn@34948
   102
  | defining_term_of_equation_term t =
bulwahn@33250
   103
    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
bulwahn@33250
   104
bulwahn@34948
   105
val defining_term_of_equation = defining_term_of_equation_term o prop_of
bulwahn@34948
   106
bulwahn@34948
   107
fun defining_const_of_equation th =
bulwahn@34948
   108
  case defining_term_of_equation th
bulwahn@34948
   109
   of Const (c, _) => c
bulwahn@34948
   110
    | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
bulwahn@34948
   111
bulwahn@34948
   112
bulwahn@34948
   113
bulwahn@33250
   114
bulwahn@33250
   115
(* Normalizing equations *)
bulwahn@33250
   116
bulwahn@33250
   117
fun mk_meta_equation th =
bulwahn@33250
   118
  case prop_of th of
haftmann@38864
   119
    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
bulwahn@33250
   120
  | _ => th
bulwahn@33250
   121
bulwahn@33250
   122
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
bulwahn@33250
   123
bulwahn@33250
   124
fun full_fun_cong_expand th =
bulwahn@33250
   125
  let
bulwahn@33250
   126
    val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
bulwahn@33250
   127
    val i = length (binder_types (fastype_of f)) - length args
bulwahn@33250
   128
  in funpow i (fn th => th RS meta_fun_cong) th end;
bulwahn@33250
   129
bulwahn@33250
   130
fun declare_names s xs ctxt =
bulwahn@33250
   131
  let
wenzelm@43329
   132
    val res = Name.invent_names ctxt s xs
bulwahn@33250
   133
  in (res, fold Name.declare (map fst res) ctxt) end
bulwahn@33250
   134
  
bulwahn@33250
   135
fun split_all_pairs thy th =
bulwahn@33250
   136
  let
wenzelm@42361
   137
    val ctxt = Proof_Context.init_global thy
bulwahn@33250
   138
    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
bulwahn@33250
   139
    val t = prop_of th'
bulwahn@33250
   140
    val frees = Term.add_frees t [] 
bulwahn@33250
   141
    val freenames = Term.add_free_names t []
bulwahn@33250
   142
    val nctxt = Name.make_context freenames
bulwahn@33250
   143
    fun mk_tuple_rewrites (x, T) nctxt =
bulwahn@33250
   144
      let
bulwahn@33250
   145
        val Ts = HOLogic.flatten_tupleT T
bulwahn@33250
   146
        val (xTs, nctxt') = declare_names x Ts nctxt
bulwahn@33250
   147
        val paths = HOLogic.flat_tupleT_paths T
bulwahn@33250
   148
      in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
bulwahn@33250
   149
    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
bulwahn@33250
   150
    val t' = Pattern.rewrite_term thy rewr [] t
bulwahn@33250
   151
    val tac = Skip_Proof.cheat_tac thy
wenzelm@33441
   152
    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
wenzelm@35624
   153
    val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
bulwahn@33250
   154
  in
bulwahn@33250
   155
    th'''
bulwahn@33250
   156
  end;
bulwahn@33250
   157
bulwahn@33250
   158
bulwahn@34948
   159
fun inline_equations thy th =
bulwahn@33404
   160
  let
wenzelm@42361
   161
    val inline_defs = Predicate_Compile_Inline_Defs.get (Proof_Context.init_global thy)
bulwahn@33404
   162
    val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
bulwahn@33404
   163
    (*val _ = print_step options 
bulwahn@33404
   164
      ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
bulwahn@33404
   165
       ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
bulwahn@33404
   166
       ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
bulwahn@33404
   167
  in
bulwahn@33404
   168
    th'
bulwahn@33404
   169
  end
bulwahn@35324
   170
bulwahn@35324
   171
fun normalize_equation thy th =
bulwahn@35324
   172
  mk_meta_equation th
bulwahn@35324
   173
  |> full_fun_cong_expand
bulwahn@35324
   174
  |> split_all_pairs thy
bulwahn@35324
   175
  |> tap check_equation_format
bulwahn@35324
   176
  |> inline_equations thy
bulwahn@33250
   177
bulwahn@35324
   178
fun normalize_intros thy th =
bulwahn@35324
   179
  split_all_pairs thy th
bulwahn@35324
   180
  |> inline_equations thy
bulwahn@35324
   181
bulwahn@35324
   182
fun normalize thy th =
bulwahn@35324
   183
  if is_equationlike th then
bulwahn@35324
   184
    normalize_equation thy th
bulwahn@35324
   185
  else
bulwahn@35324
   186
    normalize_intros thy th
bulwahn@35324
   187
bulwahn@35324
   188
fun get_specification options thy t =
bulwahn@33250
   189
  let
bulwahn@35324
   190
    (*val (c, T) = dest_Const t
bulwahn@35324
   191
    val t = Const (AxClass.unoverload_const thy (c, T), T)*)
bulwahn@35324
   192
    val _ = if show_steps options then
bulwahn@35324
   193
        tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
bulwahn@35324
   194
          " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
bulwahn@35324
   195
      else ()
wenzelm@42361
   196
    val ctxt = Proof_Context.init_global thy
bulwahn@34948
   197
    fun filtering th =
bulwahn@34948
   198
      if is_equationlike th andalso
bulwahn@35324
   199
        defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
bulwahn@34948
   200
        SOME (normalize_equation thy th)
bulwahn@34948
   201
      else
bulwahn@40142
   202
        if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
bulwahn@34948
   203
          SOME th
bulwahn@34948
   204
        else
bulwahn@34948
   205
          NONE
bulwahn@35758
   206
    fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
bulwahn@35758
   207
    val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
bulwahn@35758
   208
      [] => (case Spec_Rules.retrieve ctxt t of
bulwahn@35758
   209
          [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
bulwahn@35758
   210
        | ((_, (_, ths)) :: _) => filter_defs ths)
bulwahn@35758
   211
    | ths => rev ths
bulwahn@35324
   212
    val _ =
bulwahn@35324
   213
      if show_intermediate_results options then
wenzelm@43277
   214
        tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
bulwahn@40142
   215
          commas (map (Display.string_of_thm_global thy) spec))
bulwahn@35324
   216
      else ()
bulwahn@35324
   217
  in
bulwahn@35324
   218
    spec
bulwahn@35324
   219
  end
bulwahn@33250
   220
bulwahn@33250
   221
val logic_operator_names =
bulwahn@34948
   222
  [@{const_name "=="}, 
bulwahn@34948
   223
   @{const_name "==>"},
haftmann@38558
   224
   @{const_name Trueprop},
haftmann@38558
   225
   @{const_name Not},
haftmann@38864
   226
   @{const_name HOL.eq},
haftmann@38786
   227
   @{const_name HOL.implies},
haftmann@38558
   228
   @{const_name All},
haftmann@38558
   229
   @{const_name Ex}, 
haftmann@38795
   230
   @{const_name HOL.conj},
haftmann@38795
   231
   @{const_name HOL.disj}]
bulwahn@33250
   232
bulwahn@34948
   233
fun special_cases (c, T) = member (op =) [
haftmann@34974
   234
  @{const_name Product_Type.Unity},
haftmann@34974
   235
  @{const_name False},
haftmann@34974
   236
  @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
bulwahn@34948
   237
  @{const_name Nat.one_nat_inst.one_nat},
haftmann@35092
   238
  @{const_name Orderings.less}, @{const_name Orderings.less_eq},
haftmann@35267
   239
  @{const_name Groups.zero},
haftmann@35267
   240
  @{const_name Groups.one},  @{const_name Groups.plus},
bulwahn@34948
   241
  @{const_name Nat.ord_nat_inst.less_eq_nat},
bulwahn@34948
   242
  @{const_name Nat.ord_nat_inst.less_nat},
huffman@47108
   243
(* FIXME
bulwahn@34948
   244
  @{const_name number_nat_inst.number_of_nat},
huffman@47108
   245
*)
huffman@47108
   246
  @{const_name Num.Bit0},
huffman@47108
   247
  @{const_name Num.Bit1},
huffman@47108
   248
  @{const_name Num.One},
haftmann@34974
   249
  @{const_name Int.zero_int_inst.zero_int},
bulwahn@35324
   250
  @{const_name List.filter},
bulwahn@35324
   251
  @{const_name HOL.If},
bulwahn@35324
   252
  @{const_name Groups.minus}
bulwahn@35324
   253
  ] c
bulwahn@35324
   254
bulwahn@33250
   255
bulwahn@33252
   256
fun print_specification options thy constname specs = 
bulwahn@33252
   257
  if show_intermediate_results options then
bulwahn@33252
   258
    tracing ("Specification of " ^ constname ^ ":\n" ^
bulwahn@33252
   259
      cat_lines (map (Display.string_of_thm_global thy) specs))
bulwahn@33252
   260
  else ()
bulwahn@33252
   261
bulwahn@34948
   262
fun obtain_specification_graph options thy t =
bulwahn@33250
   263
  let
wenzelm@42361
   264
    val ctxt = Proof_Context.init_global thy
bulwahn@34948
   265
    fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
bulwahn@40053
   266
    fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c
bulwahn@34948
   267
    fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
bulwahn@34948
   268
    fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
bulwahn@33250
   269
    fun defiants_of specs =
bulwahn@34948
   270
      fold (Term.add_consts o prop_of) specs []
bulwahn@34948
   271
      |> filter_out is_datatype_constructor
bulwahn@34948
   272
      |> filter_out is_nondefining_const
bulwahn@33250
   273
      |> filter_out has_code_pred_intros
bulwahn@34948
   274
      |> filter_out case_consts
bulwahn@33250
   275
      |> filter_out special_cases
bulwahn@35324
   276
      |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c)
bulwahn@35324
   277
      |> map (fn (c, _) => (c, Sign.the_const_constraint thy c))
bulwahn@34948
   278
      |> map Const
bulwahn@34948
   279
      (*
bulwahn@34948
   280
      |> filter is_defining_constname*)
wenzelm@35405
   281
    fun extend t gr =
wenzelm@35405
   282
      if can (Term_Graph.get_node gr) t then gr
wenzelm@35405
   283
      else
wenzelm@35405
   284
        let
wenzelm@35405
   285
          val specs = get_specification options thy t
wenzelm@35405
   286
          (*val _ = print_specification options thy constname specs*)
wenzelm@35405
   287
          val us = defiants_of specs
wenzelm@35405
   288
        in
wenzelm@35405
   289
          gr
wenzelm@35405
   290
          |> Term_Graph.new_node (t, specs)
wenzelm@35405
   291
          |> fold extend us
wenzelm@35405
   292
          |> fold (fn u => Term_Graph.add_edge (t, u)) us
wenzelm@35405
   293
        end
bulwahn@33250
   294
  in
wenzelm@35405
   295
    extend t Term_Graph.empty
bulwahn@33250
   296
  end;
bulwahn@35324
   297
bulwahn@35324
   298
bulwahn@35324
   299
fun present_graph gr =
bulwahn@35324
   300
  let
bulwahn@35324
   301
    fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
bulwahn@35324
   302
    fun string_of_const (Const (c, _)) = c
bulwahn@35324
   303
      | string_of_const _ = error "string_of_const: unexpected term"
wenzelm@35404
   304
    val constss = Term_Graph.strong_conn gr;
bulwahn@35324
   305
    val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
bulwahn@35324
   306
      Termtab.update (const, consts)) consts) constss;
bulwahn@35324
   307
    fun succs consts = consts
wenzelm@44338
   308
      |> maps (Term_Graph.immediate_succs gr)
bulwahn@35324
   309
      |> subtract eq_cname consts
bulwahn@35324
   310
      |> map (the o Termtab.lookup mapping)
bulwahn@35324
   311
      |> distinct (eq_list eq_cname);
bulwahn@35324
   312
    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
bulwahn@35324
   313
    
bulwahn@35324
   314
    fun namify consts = map string_of_const consts
bulwahn@35324
   315
      |> commas;
bulwahn@35324
   316
    val prgr = map (fn (consts, constss) =>
bulwahn@35324
   317
      { name = namify consts, ID = namify consts, dir = "", unfold = true,
bulwahn@35324
   318
        path = "", parents = map namify constss }) conn;
bulwahn@35324
   319
  in Present.display_graph prgr end;
bulwahn@35324
   320
bulwahn@34948
   321
bulwahn@33250
   322
end;