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