src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author blanchet
Sun May 01 18:37:23 2011 +0200 (2011-05-01)
changeset 42520 d1f7c4a01dbe
parent 42290 b1f544c84040
child 42680 b6c27cf04fe9
permissions -rw-r--r--
renamings
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_util.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 General-purpose functions used by the Sledgehammer modules.
     5 *)
     6 
     7 signature SLEDGEHAMMER_UTIL =
     8 sig
     9   val plural_s : int -> string
    10   val serial_commas : string -> string list -> string list
    11   val simplify_spaces : string -> string
    12   val parse_bool_option : bool -> string -> string -> bool option
    13   val parse_time_option : string -> string -> Time.time option
    14   val string_from_time : Time.time -> string
    15   val nat_subscript : int -> string
    16   val unyxml : string -> string
    17   val maybe_quote : string -> string
    18   val monomorphic_term : Type.tyenv -> term -> term
    19   val eta_expand : typ list -> term -> int -> term
    20   val transform_elim_term : term -> term
    21   val specialize_type : theory -> (string * typ) -> term -> term
    22   val subgoal_count : Proof.state -> int
    23   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
    24   val reserved_isar_keyword_table : unit -> unit Symtab.table
    25 end;
    26 
    27 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    28 struct
    29 
    30 fun plural_s n = if n = 1 then "" else "s"
    31 
    32 fun serial_commas _ [] = ["??"]
    33   | serial_commas _ [s] = [s]
    34   | serial_commas conj [s1, s2] = [s1, conj, s2]
    35   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    36   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    37 
    38 val simplify_spaces = ATP_Proof.strip_spaces (K true)
    39 
    40 fun parse_bool_option option name s =
    41   (case s of
    42      "smart" => if option then NONE else raise Option
    43    | "false" => SOME false
    44    | "true" => SOME true
    45    | "" => SOME true
    46    | _ => raise Option)
    47   handle Option.Option =>
    48          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
    49            error ("Parameter " ^ quote name ^ " must be assigned " ^
    50                   space_implode " " (serial_commas "or" ss) ^ ".")
    51          end
    52 
    53 val has_junk =
    54   exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
    55 
    56 fun parse_time_option _ "none" = NONE
    57   | parse_time_option name s =
    58     let val secs = if has_junk s then NONE else Real.fromString s in
    59       if is_none secs orelse Real.<= (the secs, 0.0) then
    60         error ("Parameter " ^ quote name ^ " must be assigned a positive \
    61                \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
    62       else
    63         SOME (seconds (the secs))
    64     end
    65 
    66 fun string_from_time t =
    67   string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s"
    68 
    69 val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
    70 fun nat_subscript n =
    71   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
    72 
    73 val unyxml = XML.content_of o YXML.parse_body
    74 
    75 val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
    76 fun maybe_quote y =
    77   let val s = unyxml y in
    78     y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
    79            not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
    80            Keyword.is_keyword s) ? quote
    81   end
    82 
    83 fun monomorphic_term subst t =
    84   map_types (map_type_tvar (fn v =>
    85       case Type.lookup subst v of
    86         SOME typ => typ
    87       | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
    88                             \variable", [t]))) t
    89 
    90 fun eta_expand _ t 0 = t
    91   | eta_expand Ts (Abs (s, T, t')) n =
    92     Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
    93   | eta_expand Ts t n =
    94     fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
    95              (List.take (binder_types (fastype_of1 (Ts, t)), n))
    96              (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
    97 
    98 (* Converts an elim-rule into an equivalent theorem that does not have the
    99    predicate variable. Leaves other theorems unchanged. We simply instantiate
   100    the conclusion variable to False. (Cf. "transform_elim_theorem" in
   101    "Meson_Clausify".) *)
   102 fun transform_elim_term t =
   103   case Logic.strip_imp_concl t of
   104     @{const Trueprop} $ Var (z, @{typ bool}) =>
   105     subst_Vars [(z, @{const False})] t
   106   | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
   107   | _ => t
   108 
   109 fun specialize_type thy (s, T) t =
   110   let
   111     fun subst_for (Const (s', T')) =
   112       if s = s' then
   113         SOME (Sign.typ_match thy (T', T) Vartab.empty)
   114         handle Type.TYPE_MATCH => NONE
   115       else
   116         NONE
   117     | subst_for (t1 $ t2) =
   118       (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
   119     | subst_for (Abs (_, _, t')) = subst_for t'
   120     | subst_for _ = NONE
   121   in
   122     case subst_for t of
   123       SOME subst => monomorphic_term subst t
   124     | NONE => raise Type.TYPE_MATCH
   125   end
   126 
   127 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
   128 
   129 fun strip_subgoal goal i =
   130   let
   131     val (t, frees) = Logic.goal_params (prop_of goal) i
   132     val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
   133     val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
   134   in (rev (map dest_Free frees), hyp_ts, concl_t) end
   135 
   136 fun reserved_isar_keyword_table () =
   137   union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
   138   |> map (rpair ()) |> Symtab.make
   139 
   140 end;