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