src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
author smolkas
Fri Jul 12 19:54:36 2013 +0200 (2013-07-12 ago)
changeset 52627 ecb4a858991d
parent 52555 6811291d1869
child 54504 096f7d452164
permissions -rw-r--r--
tuned
* * *
easier debugging
* * *
tuned
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Supplements term with a locally minmal, complete set of type constraints.
     6 Complete: The constraints suffice to infer the term's types.
     7 Minimal: Reducing the set of constraints further will make it incomplete.
     8 
     9 When configuring the pretty printer appropriately, the constraints will show up
    10 as type annotations when printing the term. This allows the term to be printed
    11 and reparsed without a change of types.
    12 
    13 NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
    14 syntax.
    15 *)
    16 
    17 signature SLEDGEHAMMER_ANNOTATE =
    18 sig
    19   val annotate_types : Proof.context -> term -> term
    20 end
    21 
    22 structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
    23 struct
    24 
    25 (* Util *)
    26 fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
    27   | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
    28   | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
    29   | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
    30   | post_traverse_term_type' f env (Abs (x, T1, b)) s =
    31     let
    32       val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
    33     in f (Abs (x, T1, b')) (T1 --> T2) s' end
    34   | post_traverse_term_type' f env (u $ v) s =
    35     let
    36       val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
    37       val ((v', s''), _) = post_traverse_term_type' f env v s'
    38     in f (u' $ v') T s'' end
    39     handle Bind => raise Fail "Sledgehammer_Annotate: post_traverse_term_type'"
    40 
    41 fun post_traverse_term_type f s t =
    42   post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
    43 fun post_fold_term_type f s t =
    44   post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
    45 
    46 fun fold_map_atypes f T s =
    47   case T of
    48     Type (name, Ts) =>
    49         let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
    50           (Type (name, Ts), s)
    51         end
    52   | _ => f T s
    53 
    54 (** get unique elements of a list **)
    55 local
    56   fun unique' b x [] = if b then [x] else []
    57     | unique' b x (y :: ys) =
    58       if x = y then unique' false x ys
    59       else unique' true y ys |> b ? cons x
    60 in
    61   fun unique ord xs =
    62     case sort ord xs of x :: ys => unique' true x ys | [] => []
    63 end
    64 
    65 (** Data structures, orders **)
    66 val indexname_ord = Term_Ord.fast_indexname_ord
    67 val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
    68 structure Var_Set_Tab = Table(
    69   type key = indexname list
    70   val ord = list_ord indexname_ord)
    71 
    72 (* (1) Generalize types *)
    73 fun generalize_types ctxt t =
    74   let
    75     val erase_types = map_types (fn _ => dummyT)
    76     (* use schematic type variables *)
    77     val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
    78     val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
    79   in
    80      t |> erase_types |> infer_types
    81   end
    82 
    83 (* (2) match types *)
    84 fun match_types ctxt t1 t2 =
    85   let
    86     val thy = Proof_Context.theory_of ctxt
    87     val get_types = post_fold_term_type (K cons) []
    88   in
    89     fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
    90     handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Annotate: match_types"
    91   end
    92 
    93 
    94 (* (3) handle trivial tfrees  *)
    95 fun handle_trivial_tfrees ctxt (t', subst) =
    96   let
    97 
    98     val add_tfree_names =
    99       snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
   100 
   101     val trivial_tfree_names =
   102       Vartab.fold add_tfree_names subst []
   103       |> filter_out (Variable.is_declared ctxt)
   104       |> unique fast_string_ord
   105     val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
   106 
   107     val trivial_tvar_names =
   108       Vartab.fold
   109         (fn (tvar_name, (_, TFree (tfree_name, _))) =>
   110                tfree_name_trivial tfree_name ? cons tvar_name
   111           | _ => I)
   112         subst
   113         []
   114       |> sort indexname_ord
   115     val tvar_name_trivial = Ord_List.member indexname_ord trivial_tvar_names
   116 
   117     val t' =
   118       t' |> map_types
   119               (map_type_tvar
   120                 (fn (idxn, sort) =>
   121                   if tvar_name_trivial idxn then dummyT else TVar (idxn, sort)))
   122 
   123     val subst =
   124       subst |> fold Vartab.delete trivial_tvar_names
   125             |> Vartab.map
   126                (K (apsnd (map_type_tfree
   127                            (fn (name, sort) =>
   128                               if tfree_name_trivial name then dummyT
   129                               else TFree (name, sort)))))
   130   in
   131     (t', subst)
   132   end
   133 
   134 
   135 (* (4) Typing-spot table *)
   136 local
   137 fun key_of_atype (TVar (z, _)) =
   138     Ord_List.insert indexname_ord z
   139   | key_of_atype _ = I
   140 fun key_of_type T = fold_atyps key_of_atype T []
   141 fun update_tab t T (tab, pos) =
   142   (case key_of_type T of
   143      [] => tab
   144    | key =>
   145      let val cost = (size_of_typ T, (size_of_term t, pos)) in
   146        case Var_Set_Tab.lookup tab key of
   147          NONE => Var_Set_Tab.update_new (key, cost) tab
   148        | SOME old_cost =>
   149          (case cost_ord (cost, old_cost) of
   150             LESS => Var_Set_Tab.update (key, cost) tab
   151           | _ => tab)
   152      end,
   153    pos + 1)
   154 in
   155 val typing_spot_table =
   156   post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
   157 end
   158 
   159 (* (5) Reverse-greedy *)
   160 fun reverse_greedy typing_spot_tab =
   161   let
   162     fun update_count z =
   163       fold (fn tvar => fn tab =>
   164         let val c = Vartab.lookup tab tvar |> the_default 0 in
   165           Vartab.update (tvar, c + z) tab
   166         end)
   167     fun superfluous tcount =
   168       forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
   169     fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
   170       if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
   171       else (spot :: spots, tcount)
   172     val (typing_spots, tvar_count_tab) =
   173       Var_Set_Tab.fold
   174         (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
   175         typing_spot_tab ([], Vartab.empty)
   176       |>> sort_distinct (rev_order o cost_ord o pairself snd)
   177   in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
   178 
   179 (* (6) Introduce annotations *)
   180 fun introduce_annotations subst spots t t' =
   181   let
   182     fun subst_atype (T as TVar (idxn, S)) subst =
   183         (Envir.subst_type subst T,
   184          Vartab.update (idxn, (S, dummyT)) subst)
   185       | subst_atype T subst = (T, subst)
   186     val subst_type = fold_map_atypes subst_atype
   187     fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
   188         if p <> cp then
   189           (subst, cp + 1, ps, annots)
   190         else
   191           let val (T, subst) = subst_type T subst in
   192             (subst, cp + 1, ps', (p, T)::annots)
   193           end
   194       | collect_annot _ _ x = x
   195     val (_, _, _, annots) =
   196       post_fold_term_type collect_annot (subst, 0, spots, []) t'
   197     fun insert_annot t _ (cp, annots as (p, T) :: annots') =
   198         if p <> cp then (t, (cp + 1, annots))
   199         else (Type.constraint T t, (cp + 1, annots'))
   200       | insert_annot t _ x = (t, x)
   201   in
   202     t |> post_traverse_term_type insert_annot (0, rev annots)
   203       |> fst
   204   end
   205 
   206 (* (7) Annotate *)
   207 fun annotate_types ctxt t =
   208   let
   209     val t' = generalize_types ctxt t
   210     val subst = match_types ctxt t' t
   211     val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
   212     val typing_spots =
   213       t' |> typing_spot_table
   214          |> reverse_greedy
   215          |> sort int_ord
   216   in introduce_annotations subst typing_spots t t' end
   217 
   218 end