src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
author smolkas
Mon May 06 11:03:08 2013 +0200 (2013-05-06 ago)
changeset 51877 71052c42edf2
parent 51179 0d5f8812856f
child 52110 411db77f96f2
permissions -rw-r--r--
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
smolkas@50263
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
smolkas@50263
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50263
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50263
     4
smolkas@51179
     5
Supplement term with explicit type constraints that show up as
smolkas@50263
     6
type annotations when printing the term.
smolkas@50263
     7
*)
smolkas@50263
     8
smolkas@50258
     9
signature SLEDGEHAMMER_ANNOTATE =
smolkas@50258
    10
sig
smolkas@50258
    11
  val annotate_types : Proof.context -> term -> term
smolkas@50258
    12
end
smolkas@50258
    13
smolkas@50258
    14
structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
smolkas@50258
    15
struct
smolkas@50258
    16
smolkas@50258
    17
(* Util *)
smolkas@50258
    18
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
smolkas@50258
    19
  | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
smolkas@50258
    20
  | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
smolkas@50258
    21
  | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
smolkas@50258
    22
  | post_traverse_term_type' f env (Abs (x, T1, b)) s =
smolkas@50258
    23
    let
smolkas@50258
    24
      val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
smolkas@50258
    25
    in f (Abs (x, T1, b')) (T1 --> T2) s' end
smolkas@50258
    26
  | post_traverse_term_type' f env (u $ v) s =
smolkas@50258
    27
    let
smolkas@50258
    28
      val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
smolkas@50258
    29
      val ((v', s''), _) = post_traverse_term_type' f env v s'
smolkas@50258
    30
    in f (u' $ v') T s'' end
smolkas@50258
    31
smolkas@50258
    32
fun post_traverse_term_type f s t =
smolkas@50258
    33
  post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
smolkas@50258
    34
fun post_fold_term_type f s t =
smolkas@50258
    35
  post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
smolkas@50258
    36
smolkas@50258
    37
(* Data structures, orders *)
smolkas@50258
    38
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
smolkas@50258
    39
structure Var_Set_Tab = Table(
smolkas@50258
    40
  type key = indexname list
smolkas@50258
    41
  val ord = list_ord Term_Ord.fast_indexname_ord)
smolkas@50258
    42
smolkas@50258
    43
(* (1) Generalize types *)
smolkas@50258
    44
fun generalize_types ctxt t =
smolkas@50258
    45
  t |> map_types (fn _ => dummyT)
smolkas@50258
    46
    |> Syntax.check_term
smolkas@50258
    47
         (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
smolkas@50258
    48
smolkas@50258
    49
(* (2) Typing-spot table *)
smolkas@50258
    50
local
smolkas@50258
    51
fun key_of_atype (TVar (z, _)) =
smolkas@50258
    52
    Ord_List.insert Term_Ord.fast_indexname_ord z
smolkas@50258
    53
  | key_of_atype _ = I
smolkas@50258
    54
fun key_of_type T = fold_atyps key_of_atype T []
smolkas@50258
    55
fun update_tab t T (tab, pos) =
smolkas@50258
    56
  (case key_of_type T of
smolkas@50258
    57
     [] => tab
smolkas@50258
    58
   | key =>
smolkas@50258
    59
     let val cost = (size_of_typ T, (size_of_term t, pos)) in
smolkas@50258
    60
       case Var_Set_Tab.lookup tab key of
smolkas@50258
    61
         NONE => Var_Set_Tab.update_new (key, cost) tab
smolkas@50258
    62
       | SOME old_cost =>
smolkas@50258
    63
         (case cost_ord (cost, old_cost) of
smolkas@50258
    64
            LESS => Var_Set_Tab.update (key, cost) tab
smolkas@50258
    65
          | _ => tab)
smolkas@50258
    66
     end,
smolkas@50258
    67
   pos + 1)
smolkas@50258
    68
in
smolkas@50258
    69
val typing_spot_table =
smolkas@50258
    70
  post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
smolkas@50258
    71
end
smolkas@50258
    72
smolkas@50258
    73
(* (3) Reverse-greedy *)
smolkas@50258
    74
fun reverse_greedy typing_spot_tab =
smolkas@50258
    75
  let
smolkas@50258
    76
    fun update_count z =
smolkas@50258
    77
      fold (fn tvar => fn tab =>
smolkas@50258
    78
        let val c = Vartab.lookup tab tvar |> the_default 0 in
smolkas@50258
    79
          Vartab.update (tvar, c + z) tab
smolkas@50258
    80
        end)
smolkas@50258
    81
    fun superfluous tcount =
smolkas@50258
    82
      forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
smolkas@50258
    83
    fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
smolkas@50258
    84
      if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
smolkas@50258
    85
      else (spot :: spots, tcount)
smolkas@50258
    86
    val (typing_spots, tvar_count_tab) =
smolkas@50258
    87
      Var_Set_Tab.fold
smolkas@50258
    88
        (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
smolkas@50258
    89
        typing_spot_tab ([], Vartab.empty)
smolkas@50258
    90
      |>> sort_distinct (rev_order o cost_ord o pairself snd)
smolkas@50258
    91
  in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
smolkas@50258
    92
smolkas@50258
    93
(* (4) Introduce annotations *)
smolkas@50258
    94
fun introduce_annotations ctxt spots t t' =
smolkas@50258
    95
  let
smolkas@50258
    96
    val thy = Proof_Context.theory_of ctxt
smolkas@50258
    97
    val get_types = post_fold_term_type (K cons) []
smolkas@50258
    98
    fun match_types tp =
smolkas@50258
    99
      fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
smolkas@50258
   100
    fun unica' b x [] = if b then [x] else []
smolkas@50258
   101
      | unica' b x (y :: ys) =
smolkas@50258
   102
        if x = y then unica' false x ys
smolkas@50258
   103
        else unica' true y ys |> b ? cons x
smolkas@50258
   104
    fun unica ord xs =
smolkas@50258
   105
      case sort ord xs of x :: ys => unica' true x ys | [] => []
smolkas@50258
   106
    val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
smolkas@50258
   107
    fun erase_unica_tfrees env =
smolkas@50258
   108
      let
smolkas@50258
   109
        val unica =
smolkas@50258
   110
          Vartab.fold (add_all_tfree_namesT o snd o snd) env []
smolkas@50258
   111
          |> filter_out (Variable.is_declared ctxt)
smolkas@50258
   112
          |> unica fast_string_ord
smolkas@50258
   113
        val erase_unica = map_atyps
smolkas@50258
   114
          (fn T as TFree (s, _) =>
smolkas@50258
   115
              if Ord_List.member fast_string_ord unica s then dummyT else T
smolkas@50258
   116
            | T => T)
smolkas@50258
   117
      in Vartab.map (K (apsnd erase_unica)) env end
smolkas@50258
   118
    val env = match_types (t', t) |> erase_unica_tfrees
smolkas@50258
   119
    fun get_annot env (TFree _) = (false, (env, dummyT))
smolkas@50258
   120
      | get_annot env (T as TVar (v, S)) =
smolkas@50258
   121
        let val T' = Envir.subst_type env T in
smolkas@50258
   122
          if T' = dummyT then (false, (env, dummyT))
smolkas@50258
   123
          else (true, (Vartab.update (v, (S, dummyT)) env, T'))
smolkas@50258
   124
        end
smolkas@50258
   125
      | get_annot env (Type (S, Ts)) =
smolkas@50258
   126
        (case fold_rev (fn T => fn (b, (env, Ts)) =>
smolkas@50258
   127
                  let
smolkas@50258
   128
                    val (b', (env', T)) = get_annot env T
smolkas@50258
   129
                  in (b orelse b', (env', T :: Ts)) end)
smolkas@50258
   130
                Ts (false, (env, [])) of
smolkas@50258
   131
           (true, (env', Ts)) => (true, (env', Type (S, Ts)))
smolkas@50258
   132
         | (false, (env', _)) => (false, (env', dummyT)))
smolkas@50258
   133
    fun post1 _ T (env, cp, ps as p :: ps', annots) =
smolkas@50258
   134
        if p <> cp then
smolkas@50258
   135
          (env, cp + 1, ps, annots)
smolkas@50258
   136
        else
smolkas@51877
   137
          let val (annot_necessary, (env', T')) = get_annot env T in
smolkas@51877
   138
            (env', cp + 1, ps', annots |> annot_necessary ? cons (p, T'))
smolkas@50258
   139
          end
smolkas@50258
   140
      | post1 _ _ accum = accum
smolkas@50258
   141
    val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
smolkas@50258
   142
    fun post2 t _ (cp, annots as (p, T) :: annots') =
smolkas@50258
   143
        if p <> cp then (t, (cp + 1, annots))
smolkas@50258
   144
        else (Type.constraint T t, (cp + 1, annots'))
smolkas@50258
   145
      | post2 t _ x = (t, x)
smolkas@50258
   146
  in post_traverse_term_type post2 (0, rev annots) t |> fst end
smolkas@50258
   147
smolkas@50258
   148
(* (5) Annotate *)
smolkas@50258
   149
fun annotate_types ctxt t =
smolkas@50258
   150
  let
smolkas@50258
   151
    val t' = generalize_types ctxt t
smolkas@50258
   152
    val typing_spots =
smolkas@50258
   153
      t' |> typing_spot_table
smolkas@50258
   154
         |> reverse_greedy
smolkas@50258
   155
         |> sort int_ord
smolkas@50258
   156
  in introduce_annotations ctxt typing_spots t t' end
smolkas@50258
   157
smolkas@50258
   158
end