src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
author smolkas
Wed Jun 26 18:24:41 2013 +0200 (2013-06-26 ago)
changeset 52452 2207825d67f3
parent 52369 0b395800fdf0
child 52555 6811291d1869
permissions -rw-r--r--
ommit trivial tfrees in annotations
     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 reparsed
    11 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 
    40 fun post_traverse_term_type f s t =
    41   post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
    42 fun post_fold_term_type f s t =
    43   post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
    44 
    45 fun fold_map_atypes f T s =
    46   case T of
    47     Type (name, Ts) =>
    48         let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
    49           (Type (name, Ts), s)
    50         end
    51   | _ => f T s
    52 
    53 (** get unique elements of a list **)
    54 local
    55   fun unique' b x [] = if b then [x] else []
    56     | unique' b x (y :: ys) =
    57       if x = y then unique' false x ys
    58       else unique' true y ys |> b ? cons x
    59 in
    60   fun unique ord xs =
    61     case sort ord xs of x :: ys => unique' true x ys | [] => []
    62 end
    63 
    64 (** Data structures, orders **)
    65 val indexname_ord = Term_Ord.fast_indexname_ord
    66 val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
    67 structure Var_Set_Tab = Table(
    68   type key = indexname list
    69   val ord = list_ord indexname_ord)
    70 
    71 (* (1) Generalize types *)
    72 fun generalize_types ctxt t =
    73   let
    74     val erase_types = map_types (fn _ => dummyT)
    75     (* use schematic type variables *)
    76     val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
    77     val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
    78   in
    79      t |> erase_types |> infer_types
    80   end
    81 
    82 (* (2) match types *)
    83 fun match_types ctxt t1 t2 =
    84   let
    85     val thy = Proof_Context.theory_of ctxt
    86     val get_types = post_fold_term_type (K cons) []
    87   in
    88     fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
    89   end
    90 
    91 
    92 (* (3) handle trivial tfrees  *)
    93 fun handle_trivial_tfrees ctxt (t', subst) =
    94   let
    95 
    96     val add_tfree_names =
    97       snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
    98 
    99     val trivial_tfree_names =
   100       Vartab.fold add_tfree_names subst []
   101       |> filter_out (Variable.is_declared ctxt)
   102       |> unique fast_string_ord
   103     val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
   104 
   105     val trivial_tvar_names =
   106       Vartab.fold
   107         (fn (tvar_name, (_, TFree (tfree_name, _))) =>
   108                tfree_name_trivial tfree_name ? cons tvar_name
   109           | _ => I)
   110         subst
   111         []
   112       |> sort indexname_ord
   113     val tvar_name_trivial = Ord_List.member indexname_ord trivial_tvar_names
   114 
   115     val t' =
   116       t' |> map_types
   117               (map_type_tvar
   118                 (fn (idxn, sort) =>
   119                   if tvar_name_trivial idxn then dummyT else TVar (idxn, sort)))
   120 
   121     val subst =
   122       subst |> fold Vartab.delete trivial_tvar_names
   123             |> Vartab.map
   124                (K (apsnd (map_type_tfree
   125                            (fn (name, sort) =>
   126                               if tfree_name_trivial name then dummyT
   127                               else TFree (name, sort)))))
   128   in
   129     (t', subst)
   130   end
   131 
   132 
   133 (* (4) Typing-spot table *)
   134 local
   135 fun key_of_atype (TVar (z, _)) =
   136     Ord_List.insert indexname_ord z
   137   | key_of_atype _ = I
   138 fun key_of_type T = fold_atyps key_of_atype T []
   139 fun update_tab t T (tab, pos) =
   140   (case key_of_type T of
   141      [] => tab
   142    | key =>
   143      let val cost = (size_of_typ T, (size_of_term t, pos)) in
   144        case Var_Set_Tab.lookup tab key of
   145          NONE => Var_Set_Tab.update_new (key, cost) tab
   146        | SOME old_cost =>
   147          (case cost_ord (cost, old_cost) of
   148             LESS => Var_Set_Tab.update (key, cost) tab
   149           | _ => tab)
   150      end,
   151    pos + 1)
   152 in
   153 val typing_spot_table =
   154   post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
   155 end
   156 
   157 (* (5) Reverse-greedy *)
   158 fun reverse_greedy typing_spot_tab =
   159   let
   160     fun update_count z =
   161       fold (fn tvar => fn tab =>
   162         let val c = Vartab.lookup tab tvar |> the_default 0 in
   163           Vartab.update (tvar, c + z) tab
   164         end)
   165     fun superfluous tcount =
   166       forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
   167     fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
   168       if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
   169       else (spot :: spots, tcount)
   170     val (typing_spots, tvar_count_tab) =
   171       Var_Set_Tab.fold
   172         (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
   173         typing_spot_tab ([], Vartab.empty)
   174       |>> sort_distinct (rev_order o cost_ord o pairself snd)
   175   in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
   176 
   177 (* (6) Introduce annotations *)
   178 fun introduce_annotations subst spots t t' =
   179   let
   180     fun subst_atype (T as TVar (idxn, S)) subst =
   181         (Envir.subst_type subst T,
   182          Vartab.update (idxn, (S, dummyT)) subst)
   183       | subst_atype T subst = (T, subst)
   184     val subst_type = fold_map_atypes subst_atype
   185     fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
   186         if p <> cp then
   187           (subst, cp + 1, ps, annots)
   188         else
   189           let val (T, subst) = subst_type T subst in
   190             (subst, cp + 1, ps', (p, T)::annots)
   191           end
   192       | collect_annot _ _ x = x
   193     val (_, _, _, annots) =
   194       post_fold_term_type collect_annot (subst, 0, spots, []) t'
   195     fun insert_annot t _ (cp, annots as (p, T) :: annots') =
   196         if p <> cp then (t, (cp + 1, annots))
   197         else (Type.constraint T t, (cp + 1, annots'))
   198       | insert_annot t _ x = (t, x)
   199   in
   200     t |> post_traverse_term_type insert_annot (0, rev annots)
   201       |> fst
   202   end
   203 
   204 (* (7) Annotate *)
   205 fun annotate_types ctxt t =
   206   let
   207     val t' = generalize_types ctxt t
   208     val subst = match_types ctxt t' t
   209     val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
   210     val typing_spots =
   211       t' |> typing_spot_table
   212          |> reverse_greedy
   213          |> sort int_ord
   214   in introduce_annotations subst typing_spots t t' end
   215 
   216 end