src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 40053 3fa49ea76cbb
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
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@33250
    77
(*TODO*)
bulwahn@33250
    78
fun is_introlike_term t = true
bulwahn@33250
    79
bulwahn@33250
    80
val is_introlike = is_introlike_term o prop_of
bulwahn@33250
    81
bulwahn@33250
    82
fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
bulwahn@33250
    83
  (case strip_comb u of
bulwahn@33250
    84
    (Const (c, T), args) =>
bulwahn@33250
    85
      if (length (binder_types T) = length args) then
bulwahn@33250
    86
        true
bulwahn@33250
    87
      else
bulwahn@33250
    88
        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
bulwahn@33250
    89
  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
bulwahn@33250
    90
  | check_equation_format_term t =
bulwahn@33250
    91
    raise TERM ("check_equation_format_term failed: Not an equation", [t])
bulwahn@33250
    92
bulwahn@33250
    93
val check_equation_format = check_equation_format_term o prop_of
bulwahn@33250
    94
bulwahn@34948
    95
bulwahn@34948
    96
fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u)
bulwahn@34948
    97
  | defining_term_of_equation_term t =
bulwahn@33250
    98
    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
bulwahn@33250
    99
bulwahn@34948
   100
val defining_term_of_equation = defining_term_of_equation_term o prop_of
bulwahn@34948
   101
bulwahn@34948
   102
fun defining_const_of_equation th =
bulwahn@34948
   103
  case defining_term_of_equation th
bulwahn@34948
   104
   of Const (c, _) => c
bulwahn@34948
   105
    | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
bulwahn@34948
   106
bulwahn@34948
   107
bulwahn@34948
   108
bulwahn@33250
   109
bulwahn@33250
   110
(* Normalizing equations *)
bulwahn@33250
   111
bulwahn@33250
   112
fun mk_meta_equation th =
bulwahn@33250
   113
  case prop_of th of
haftmann@38864
   114
    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
bulwahn@33250
   115
  | _ => th
bulwahn@33250
   116
bulwahn@33250
   117
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
bulwahn@33250
   118
bulwahn@33250
   119
fun full_fun_cong_expand th =
bulwahn@33250
   120
  let
bulwahn@33250
   121
    val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
bulwahn@33250
   122
    val i = length (binder_types (fastype_of f)) - length args
bulwahn@33250
   123
  in funpow i (fn th => th RS meta_fun_cong) th end;
bulwahn@33250
   124
bulwahn@33250
   125
fun declare_names s xs ctxt =
bulwahn@33250
   126
  let
bulwahn@33250
   127
    val res = Name.names ctxt s xs
bulwahn@33250
   128
  in (res, fold Name.declare (map fst res) ctxt) end
bulwahn@33250
   129
  
bulwahn@33250
   130
fun split_all_pairs thy th =
bulwahn@33250
   131
  let
wenzelm@36610
   132
    val ctxt = ProofContext.init_global thy
bulwahn@33250
   133
    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
bulwahn@33250
   134
    val t = prop_of th'
bulwahn@33250
   135
    val frees = Term.add_frees t [] 
bulwahn@33250
   136
    val freenames = Term.add_free_names t []
bulwahn@33250
   137
    val nctxt = Name.make_context freenames
bulwahn@33250
   138
    fun mk_tuple_rewrites (x, T) nctxt =
bulwahn@33250
   139
      let
bulwahn@33250
   140
        val Ts = HOLogic.flatten_tupleT T
bulwahn@33250
   141
        val (xTs, nctxt') = declare_names x Ts nctxt
bulwahn@33250
   142
        val paths = HOLogic.flat_tupleT_paths T
bulwahn@33250
   143
      in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
bulwahn@33250
   144
    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
bulwahn@33250
   145
    val t' = Pattern.rewrite_term thy rewr [] t
bulwahn@33250
   146
    val tac = Skip_Proof.cheat_tac thy
wenzelm@33441
   147
    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
wenzelm@35624
   148
    val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
bulwahn@33250
   149
  in
bulwahn@33250
   150
    th'''
bulwahn@33250
   151
  end;
bulwahn@33250
   152
bulwahn@33250
   153
bulwahn@34948
   154
fun inline_equations thy th =
bulwahn@33404
   155
  let
wenzelm@36610
   156
    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init_global thy)
bulwahn@33404
   157
    val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
bulwahn@33404
   158
    (*val _ = print_step options 
bulwahn@33404
   159
      ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
bulwahn@33404
   160
       ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
bulwahn@33404
   161
       ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
bulwahn@33404
   162
  in
bulwahn@33404
   163
    th'
bulwahn@33404
   164
  end
bulwahn@35324
   165
bulwahn@35324
   166
fun normalize_equation thy th =
bulwahn@35324
   167
  mk_meta_equation th
bulwahn@35324
   168
  |> full_fun_cong_expand
bulwahn@35324
   169
  |> split_all_pairs thy
bulwahn@35324
   170
  |> tap check_equation_format
bulwahn@35324
   171
  |> inline_equations thy
bulwahn@33250
   172
bulwahn@35324
   173
fun normalize_intros thy th =
bulwahn@35324
   174
  split_all_pairs thy th
bulwahn@35324
   175
  |> inline_equations thy
bulwahn@35324
   176
bulwahn@35324
   177
fun normalize thy th =
bulwahn@35324
   178
  if is_equationlike th then
bulwahn@35324
   179
    normalize_equation thy th
bulwahn@35324
   180
  else
bulwahn@35324
   181
    normalize_intros thy th
bulwahn@35324
   182
bulwahn@35324
   183
fun get_specification options thy t =
bulwahn@33250
   184
  let
bulwahn@35324
   185
    (*val (c, T) = dest_Const t
bulwahn@35324
   186
    val t = Const (AxClass.unoverload_const thy (c, T), T)*)
bulwahn@35324
   187
    val _ = if show_steps options then
bulwahn@35324
   188
        tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
bulwahn@35324
   189
          " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
bulwahn@35324
   190
      else ()
wenzelm@36610
   191
    val ctxt = ProofContext.init_global thy
bulwahn@34948
   192
    fun filtering th =
bulwahn@34948
   193
      if is_equationlike th andalso
bulwahn@35324
   194
        defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
bulwahn@34948
   195
        SOME (normalize_equation thy th)
bulwahn@34948
   196
      else
bulwahn@34948
   197
        if is_introlike th andalso defining_term_of_introrule th = t then
bulwahn@34948
   198
          SOME th
bulwahn@34948
   199
        else
bulwahn@34948
   200
          NONE
bulwahn@35758
   201
    fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
bulwahn@35758
   202
    val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
bulwahn@35758
   203
      [] => (case Spec_Rules.retrieve ctxt t of
bulwahn@35758
   204
          [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
bulwahn@35758
   205
        | ((_, (_, ths)) :: _) => filter_defs ths)
bulwahn@35758
   206
    | ths => rev ths
bulwahn@35324
   207
    val _ =
bulwahn@35324
   208
      if show_intermediate_results options then
bulwahn@35324
   209
        Output.tracing (commas (map (Display.string_of_thm_global thy) spec))
bulwahn@35324
   210
      else ()
bulwahn@35324
   211
  in
bulwahn@35324
   212
    spec
bulwahn@35324
   213
  end
bulwahn@33250
   214
bulwahn@33250
   215
val logic_operator_names =
bulwahn@34948
   216
  [@{const_name "=="}, 
bulwahn@34948
   217
   @{const_name "==>"},
haftmann@38558
   218
   @{const_name Trueprop},
haftmann@38558
   219
   @{const_name Not},
haftmann@38864
   220
   @{const_name HOL.eq},
haftmann@38786
   221
   @{const_name HOL.implies},
haftmann@38558
   222
   @{const_name All},
haftmann@38558
   223
   @{const_name Ex}, 
haftmann@38795
   224
   @{const_name HOL.conj},
haftmann@38795
   225
   @{const_name HOL.disj}]
bulwahn@33250
   226
bulwahn@34948
   227
fun special_cases (c, T) = member (op =) [
haftmann@34974
   228
  @{const_name Product_Type.Unity},
haftmann@34974
   229
  @{const_name False},
haftmann@34974
   230
  @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
bulwahn@34948
   231
  @{const_name Nat.one_nat_inst.one_nat},
haftmann@35092
   232
  @{const_name Orderings.less}, @{const_name Orderings.less_eq},
haftmann@35267
   233
  @{const_name Groups.zero},
haftmann@35267
   234
  @{const_name Groups.one},  @{const_name Groups.plus},
bulwahn@34948
   235
  @{const_name Nat.ord_nat_inst.less_eq_nat},
bulwahn@34948
   236
  @{const_name Nat.ord_nat_inst.less_nat},
bulwahn@34948
   237
  @{const_name number_nat_inst.number_of_nat},
bulwahn@33250
   238
  @{const_name Int.Bit0},
bulwahn@33250
   239
  @{const_name Int.Bit1},
bulwahn@33250
   240
  @{const_name Int.Pls},
haftmann@34974
   241
  @{const_name Int.zero_int_inst.zero_int},
bulwahn@35324
   242
  @{const_name List.filter},
bulwahn@35324
   243
  @{const_name HOL.If},
bulwahn@35324
   244
  @{const_name Groups.minus}
bulwahn@35324
   245
  ] c
bulwahn@35324
   246
bulwahn@33250
   247
bulwahn@33252
   248
fun print_specification options thy constname specs = 
bulwahn@33252
   249
  if show_intermediate_results options then
bulwahn@33252
   250
    tracing ("Specification of " ^ constname ^ ":\n" ^
bulwahn@33252
   251
      cat_lines (map (Display.string_of_thm_global thy) specs))
bulwahn@33252
   252
  else ()
bulwahn@33252
   253
bulwahn@34948
   254
fun obtain_specification_graph options thy t =
bulwahn@33250
   255
  let
bulwahn@37007
   256
    val ctxt = ProofContext.init_global thy
bulwahn@34948
   257
    fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
bulwahn@37007
   258
    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c
bulwahn@34948
   259
    fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
bulwahn@34948
   260
    fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
bulwahn@33250
   261
    fun defiants_of specs =
bulwahn@34948
   262
      fold (Term.add_consts o prop_of) specs []
bulwahn@34948
   263
      |> filter_out is_datatype_constructor
bulwahn@34948
   264
      |> filter_out is_nondefining_const
bulwahn@33250
   265
      |> filter_out has_code_pred_intros
bulwahn@34948
   266
      |> filter_out case_consts
bulwahn@33250
   267
      |> filter_out special_cases
bulwahn@35324
   268
      |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c)
bulwahn@35324
   269
      |> map (fn (c, _) => (c, Sign.the_const_constraint thy c))
bulwahn@34948
   270
      |> map Const
bulwahn@34948
   271
      (*
bulwahn@34948
   272
      |> filter is_defining_constname*)
wenzelm@35405
   273
    fun extend t gr =
wenzelm@35405
   274
      if can (Term_Graph.get_node gr) t then gr
wenzelm@35405
   275
      else
wenzelm@35405
   276
        let
wenzelm@35405
   277
          val specs = get_specification options thy t
wenzelm@35405
   278
          (*val _ = print_specification options thy constname specs*)
wenzelm@35405
   279
          val us = defiants_of specs
wenzelm@35405
   280
        in
wenzelm@35405
   281
          gr
wenzelm@35405
   282
          |> Term_Graph.new_node (t, specs)
wenzelm@35405
   283
          |> fold extend us
wenzelm@35405
   284
          |> fold (fn u => Term_Graph.add_edge (t, u)) us
wenzelm@35405
   285
        end
bulwahn@33250
   286
  in
wenzelm@35405
   287
    extend t Term_Graph.empty
bulwahn@33250
   288
  end;
bulwahn@35324
   289
bulwahn@35324
   290
bulwahn@35324
   291
fun present_graph gr =
bulwahn@35324
   292
  let
bulwahn@35324
   293
    fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
bulwahn@35324
   294
    fun string_of_const (Const (c, _)) = c
bulwahn@35324
   295
      | string_of_const _ = error "string_of_const: unexpected term"
wenzelm@35404
   296
    val constss = Term_Graph.strong_conn gr;
bulwahn@35324
   297
    val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
bulwahn@35324
   298
      Termtab.update (const, consts)) consts) constss;
bulwahn@35324
   299
    fun succs consts = consts
wenzelm@35404
   300
      |> maps (Term_Graph.imm_succs gr)
bulwahn@35324
   301
      |> subtract eq_cname consts
bulwahn@35324
   302
      |> map (the o Termtab.lookup mapping)
bulwahn@35324
   303
      |> distinct (eq_list eq_cname);
bulwahn@35324
   304
    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
bulwahn@35324
   305
    
bulwahn@35324
   306
    fun namify consts = map string_of_const consts
bulwahn@35324
   307
      |> commas;
bulwahn@35324
   308
    val prgr = map (fn (consts, constss) =>
bulwahn@35324
   309
      { name = namify consts, ID = namify consts, dir = "", unfold = true,
bulwahn@35324
   310
        path = "", parents = map namify constss }) conn;
bulwahn@35324
   311
  in Present.display_graph prgr end;
bulwahn@35324
   312
bulwahn@34948
   313
bulwahn@33250
   314
end;