prevent pretty printer from automatically annotating numerals
authorsmolkas
Wed May 22 12:39:09 2013 +0200 (2013-05-22 ago)
changeset 52110411db77f96f2
parent 52109 39ac12f31f5c
child 52117 352ea4b159ff
prevent pretty printer from automatically annotating numerals
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed May 22 12:39:07 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed May 22 12:39:09 2013 +0200
     1.3 @@ -34,6 +34,19 @@
     1.4  fun post_fold_term_type f s t =
     1.5    post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
     1.6  
     1.7 +local
     1.8 +fun natify_numeral' (t as Const (s, T)) =
     1.9 +    (case s of
    1.10 +      "Groups.zero_class.zero" => Const (s, @{typ "nat"})
    1.11 +    | "Groups.one_class.one" => Const (s, @{typ "nat"})
    1.12 +    | "Num.numeral_class.numeral" => Const(s, @{typ "num"} --> @{typ "nat"})
    1.13 +    | "Num.numeral_class.neg_numeral" => Const(s, @{typ "num"} --> @{typ "nat"})
    1.14 +    | _ => t)
    1.15 +  | natify_numeral' t = t
    1.16 +in
    1.17 +val natify_numerals = Term.map_aterms natify_numeral'
    1.18 +end
    1.19 +
    1.20  (* Data structures, orders *)
    1.21  val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
    1.22  structure Var_Set_Tab = Table(
    1.23 @@ -143,7 +156,12 @@
    1.24          if p <> cp then (t, (cp + 1, annots))
    1.25          else (Type.constraint T t, (cp + 1, annots'))
    1.26        | post2 t _ x = (t, x)
    1.27 -  in post_traverse_term_type post2 (0, rev annots) t |> fst end
    1.28 +  in
    1.29 +    t |> natify_numerals (* typing all numerals as "nat"s prevents the pretty
    1.30 +         printer from inserting additional, unwanted type annotations *)
    1.31 +      |> post_traverse_term_type post2 (0, rev annots)
    1.32 +      |> fst
    1.33 +  end
    1.34  
    1.35  (* (5) Annotate *)
    1.36  fun annotate_types ctxt t =