added options to Sledgehammer;
authorblanchet
Tue Mar 23 11:39:21 2010 +0100 (2010-03-23)
changeset 35963943e2582dc87
parent 35962 0e2d57686b3c
child 35964 77f2cb359b49
added options to Sledgehammer;
syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Mar 22 15:23:18 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Mar 23 11:39:21 2010 +0100
     1.3 @@ -12,9 +12,11 @@
     1.4    val tvar_classes_of_terms : term list -> string list
     1.5    val tfree_classes_of_terms : term list -> string list
     1.6    val type_consts_of_terms : theory -> term list -> string list
     1.7 -  val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
     1.8 -    (thm * (string * int)) list
     1.9 -  val prepare_clauses : bool -> thm list -> thm list ->
    1.10 +  val get_relevant_facts :
    1.11 +    real -> bool option -> bool -> int -> bool
    1.12 +    -> Proof.context * (thm list * 'a) -> thm list
    1.13 +    -> (thm * (string * int)) list
    1.14 +  val prepare_clauses : bool option -> bool -> thm list -> thm list ->
    1.15      (thm * (axiom_name * hol_clause_id)) list ->
    1.16      (thm * (axiom_name * hol_clause_id)) list -> theory ->
    1.17      axiom_name vector *
    1.18 @@ -38,20 +40,11 @@
    1.19  (* and also explicit ATP invocation methods                         *)
    1.20  (********************************************************************)
    1.21  
    1.22 -(* Translation mode can be auto-detected, or forced to be first-order or
    1.23 -   higher-order *)
    1.24 -datatype mode = Auto | Fol | Hol;
    1.25 -
    1.26 -val translation_mode = Auto;
    1.27 -
    1.28  (*** background linkup ***)
    1.29  val run_blacklist_filter = true;
    1.30  
    1.31  (*** relevance filter parameters ***)
    1.32 -val run_relevance_filter = true;
    1.33 -val pass_mark = 0.5;
    1.34  val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
    1.35 -val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
    1.36    
    1.37  (***************************************************************)
    1.38  (* Relevance Filtering                                         *)
    1.39 @@ -139,8 +132,8 @@
    1.40  
    1.41  (*Inserts a dummy "constant" referring to the theory name, so that relevance
    1.42    takes the given theory into account.*)
    1.43 -fun const_prop_of theory_const th =
    1.44 - if theory_const then
    1.45 +fun const_prop_of add_theory_const th =
    1.46 + if add_theory_const then
    1.47    let val name = Context.theory_name (theory_of_thm th)
    1.48        val t = Const (name ^ ". 1", HOLogic.boolT)
    1.49    in  t $ prop_of th  end
    1.50 @@ -169,7 +162,7 @@
    1.51  
    1.52  structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
    1.53  
    1.54 -fun count_axiom_consts theory_const thy ((thm,_), tab) = 
    1.55 +fun count_axiom_consts add_theory_const thy ((thm,_), tab) = 
    1.56    let fun count_const (a, T, tab) =
    1.57          let val (c, cts) = const_with_typ thy (a,T)
    1.58          in  (*Two-dimensional table update. Constant maps to types maps to count.*)
    1.59 @@ -182,7 +175,7 @@
    1.60              count_term_consts (t, count_term_consts (u, tab))
    1.61          | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
    1.62          | count_term_consts (_, tab) = tab
    1.63 -  in  count_term_consts (const_prop_of theory_const thm, tab)  end;
    1.64 +  in  count_term_consts (const_prop_of add_theory_const thm, tab)  end;
    1.65  
    1.66  
    1.67  (**** Actual Filtering Code ****)
    1.68 @@ -214,8 +207,8 @@
    1.69    let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
    1.70    in  Symtab.fold add_expand_pairs tab []  end;
    1.71  
    1.72 -fun pair_consts_typs_axiom theory_const thy (thm,name) =
    1.73 -    ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
    1.74 +fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) =
    1.75 +  (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm)));
    1.76  
    1.77  exception ConstFree;
    1.78  fun dest_ConstFree (Const aT) = aT
    1.79 @@ -234,9 +227,10 @@
    1.80              end
    1.81              handle ConstFree => false
    1.82      in    
    1.83 -        case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) => 
    1.84 -                   defs lhs rhs 
    1.85 -                 | _ => false
    1.86 +        case tm of
    1.87 +          @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => 
    1.88 +            defs lhs rhs 
    1.89 +        | _ => false
    1.90      end;
    1.91  
    1.92  type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
    1.93 @@ -263,7 +257,7 @@
    1.94        end
    1.95    end;
    1.96  
    1.97 -fun relevant_clauses max_new thy ctab p rel_consts =
    1.98 +fun relevant_clauses follow_defs max_new thy ctab p rel_consts =
    1.99    let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
   1.100          | relevant (newpairs,rejects) [] =
   1.101              let val (newrels,more_rejects) = take_best max_new newpairs
   1.102 @@ -273,7 +267,8 @@
   1.103              in
   1.104                trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
   1.105                 (map #1 newrels) @ 
   1.106 -               (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
   1.107 +               (relevant_clauses follow_defs max_new thy ctab newp rel_consts'
   1.108 +                                 (more_rejects @ rejects))
   1.109              end
   1.110          | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   1.111              let val weight = clause_weight ctab rel_consts consts_typs
   1.112 @@ -288,20 +283,27 @@
   1.113          relevant ([],[]) 
   1.114      end;
   1.115          
   1.116 -fun relevance_filter max_new theory_const thy axioms goals = 
   1.117 - if run_relevance_filter andalso pass_mark >= 0.1
   1.118 - then
   1.119 -  let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
   1.120 +fun relevance_filter relevance_threshold follow_defs max_new add_theory_const
   1.121 +                     thy axioms goals = 
   1.122 +  if relevance_threshold >= 0.1 then
   1.123 +    let
   1.124 +      val const_tab = List.foldl (count_axiom_consts add_theory_const thy)
   1.125 +                                 Symtab.empty axioms
   1.126        val goal_const_tab = get_goal_consts_typs thy goals
   1.127 -      val _ = trace_msg (fn () => ("Initial constants: " ^
   1.128 -                                 space_implode ", " (Symtab.keys goal_const_tab)));
   1.129 -      val rels = relevant_clauses max_new thy const_tab (pass_mark) 
   1.130 -                   goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
   1.131 -  in
   1.132 -      trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   1.133 -      rels
   1.134 -  end
   1.135 - else axioms;
   1.136 +      val _ =
   1.137 +        trace_msg (fn () => "Initial constants: " ^
   1.138 +                            commas (Symtab.keys goal_const_tab))
   1.139 +      val relevant =
   1.140 +        relevant_clauses follow_defs max_new thy const_tab
   1.141 +                         relevance_threshold goal_const_tab
   1.142 +                         (map (pair_consts_typs_axiom add_theory_const thy)
   1.143 +                              axioms)
   1.144 +    in
   1.145 +      trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
   1.146 +      relevant
   1.147 +    end
   1.148 +  else
   1.149 +    axioms;
   1.150  
   1.151  (***************************************************************)
   1.152  (* Retrieving and filtering lemmas                             *)
   1.153 @@ -526,34 +528,35 @@
   1.154    likely to lead to unsound proofs.*)
   1.155  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   1.156  
   1.157 -fun is_first_order thy goal_cls =
   1.158 -  case translation_mode of
   1.159 -    Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   1.160 -  | Fol => true
   1.161 -  | Hol => false
   1.162 +fun is_first_order thy higher_order goal_cls =
   1.163 +  case higher_order of
   1.164 +    NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   1.165 +  | SOME b => not b
   1.166  
   1.167 -fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   1.168 +fun get_relevant_facts relevance_threshold higher_order follow_defs max_new
   1.169 +                       add_theory_const (ctxt, (chain_ths, th)) goal_cls =
   1.170    let
   1.171      val thy = ProofContext.theory_of ctxt
   1.172 -    val is_FO = is_first_order thy goal_cls
   1.173 +    val is_FO = is_first_order thy higher_order goal_cls
   1.174      val included_cls = get_all_lemmas ctxt
   1.175        |> cnf_rules_pairs thy |> make_unique
   1.176        |> restrict_to_logic thy is_FO
   1.177        |> remove_unwanted_clauses
   1.178    in
   1.179 -    relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) 
   1.180 +    relevance_filter relevance_threshold follow_defs max_new add_theory_const
   1.181 +                     thy included_cls (map prop_of goal_cls)
   1.182    end;
   1.183  
   1.184  (* prepare for passing to writer,
   1.185     create additional clauses based on the information from extra_cls *)
   1.186 -fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   1.187 +fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
   1.188    let
   1.189      (* add chain thms *)
   1.190      val chain_cls =
   1.191        cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
   1.192      val axcls = chain_cls @ axcls
   1.193      val extra_cls = chain_cls @ extra_cls
   1.194 -    val is_FO = is_first_order thy goal_cls
   1.195 +    val is_FO = is_first_order thy higher_order goal_cls
   1.196      val ccls = subtract_cls goal_cls extra_cls
   1.197      val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   1.198      val ccltms = map prop_of ccls
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Mar 22 15:23:18 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Mar 23 11:39:21 2010 +0100
     2.3 @@ -51,9 +51,9 @@
     2.4    conclusion variable to False.*)
     2.5  fun transform_elim th =
     2.6    case concl_of th of    (*conclusion variable*)
     2.7 -       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
     2.8 +       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
     2.9             Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    2.10 -    | v as Var(_, Type("prop",[])) =>
    2.11 +    | v as Var(_, @{typ prop}) =>
    2.12             Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    2.13      | _ => th;
    2.14  
    2.15 @@ -76,7 +76,7 @@
    2.16  fun declare_skofuns s th =
    2.17    let
    2.18      val nref = Unsynchronized.ref 0    (* FIXME ??? *)
    2.19 -    fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
    2.20 +    fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
    2.21            (*Existential: declare a Skolem function, then insert into body and continue*)
    2.22            let
    2.23              val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
    2.24 @@ -95,20 +95,20 @@
    2.25                Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
    2.26              val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
    2.27            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
    2.28 -      | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
    2.29 +      | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
    2.30            (*Universal quant: insert a free variable into body and continue*)
    2.31            let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
    2.32            in dec_sko (subst_bound (Free (fname, T), p)) thx end
    2.33 -      | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
    2.34 -      | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
    2.35 -      | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
    2.36 +      | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
    2.37 +      | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
    2.38 +      | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
    2.39        | dec_sko t thx = thx (*Do nothing otherwise*)
    2.40    in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
    2.41  
    2.42  (*Traverse a theorem, accumulating Skolem function definitions.*)
    2.43  fun assume_skofuns s th =
    2.44    let val sko_count = Unsynchronized.ref 0   (* FIXME ??? *)
    2.45 -      fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
    2.46 +      fun dec_sko (Const (@{const_name "Ex"}, _) $ (xtp as Abs(_,T,p))) defs =
    2.47              (*Existential: declare a Skolem function, then insert into body and continue*)
    2.48              let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
    2.49                  val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
    2.50 @@ -123,13 +123,13 @@
    2.51              in dec_sko (subst_bound (list_comb(c,args), p))
    2.52                         (def :: defs)
    2.53              end
    2.54 -        | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs =
    2.55 +        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
    2.56              (*Universal quant: insert a free variable into body and continue*)
    2.57              let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    2.58              in dec_sko (subst_bound (Free(fname,T), p)) defs end
    2.59 -        | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
    2.60 -        | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
    2.61 -        | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
    2.62 +        | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
    2.63 +        | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
    2.64 +        | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
    2.65          | dec_sko t defs = defs (*Do nothing otherwise*)
    2.66    in  dec_sko (prop_of th) []  end;
    2.67  
    2.68 @@ -156,7 +156,7 @@
    2.69  fun strip_lambdas 0 th = th
    2.70    | strip_lambdas n th =
    2.71        case prop_of th of
    2.72 -          _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
    2.73 +          _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
    2.74                strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
    2.75          | _ => th;
    2.76  
    2.77 @@ -171,7 +171,7 @@
    2.78    let
    2.79        val thy = theory_of_cterm ct
    2.80        val Abs(x,_,body) = term_of ct
    2.81 -      val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
    2.82 +      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
    2.83        val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
    2.84        fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
    2.85    in
    2.86 @@ -262,8 +262,9 @@
    2.87        val (chilbert,cabs) = Thm.dest_comb ch
    2.88        val thy = Thm.theory_of_cterm chilbert
    2.89        val t = Thm.term_of chilbert
    2.90 -      val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
    2.91 -                      | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
    2.92 +      val T = case t of
    2.93 +                Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
    2.94 +              | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
    2.95        val cex = Thm.cterm_of thy (HOLogic.exists_const T)
    2.96        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
    2.97        and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
    2.98 @@ -289,7 +290,7 @@
    2.99    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
   2.100  
   2.101  
   2.102 -(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***)
   2.103 +(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
   2.104  
   2.105  val max_lambda_nesting = 3;
   2.106  
   2.107 @@ -320,7 +321,8 @@
   2.108  
   2.109  fun is_strange_thm th =
   2.110    case head_of (concl_of th) of
   2.111 -      Const (a, _) => (a <> "Trueprop" andalso a <> "==")
   2.112 +      Const (a, _) => (a <> @{const_name Trueprop} andalso
   2.113 +                       a <> @{const_name "=="})
   2.114      | _ => false;
   2.115  
   2.116  fun bad_for_atp th =
   2.117 @@ -328,9 +330,10 @@
   2.118    orelse exists_type type_has_topsort (prop_of th)
   2.119    orelse is_strange_thm th;
   2.120  
   2.121 +(* FIXME: put other record thms here, or declare as "no_atp" *)
   2.122  val multi_base_blacklist =
   2.123 -  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
   2.124 -   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "no_atp" *)
   2.125 +  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
   2.126 +   "split_asm", "cases", "ext_cases"];
   2.127  
   2.128  (*Keep the full complexity of the original name*)
   2.129  fun flatten_name s = space_implode "_X" (Long_Name.explode s);
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Mar 22 15:23:18 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Mar 23 11:39:21 2010 +0100
     3.3 @@ -48,7 +48,7 @@
     3.4  open Sledgehammer_FOL_Clause
     3.5  open Sledgehammer_Fact_Preprocessor
     3.6  
     3.7 -(* Parameter t_full below indicates that full type information is to be
     3.8 +(* Parameter "full_types" below indicates that full type information is to be
     3.9  exported *)
    3.10  
    3.11  (* If true, each function will be directly applied to as many arguments as
    3.12 @@ -210,10 +210,8 @@
    3.13  fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
    3.14    | head_needs_hBOOL _ _ = true;
    3.15  
    3.16 -fun wrap_type t_full (s, tp) =
    3.17 -  if t_full then
    3.18 -      type_wrapper ^ paren_pack [s, string_of_fol_type tp]
    3.19 -  else s;
    3.20 +fun wrap_type full_types (s, tp) =
    3.21 +  if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
    3.22  
    3.23  fun apply ss = "hAPP" ^ paren_pack ss;
    3.24  
    3.25 @@ -224,7 +222,7 @@
    3.26  
    3.27  (*Apply an operator to the argument strings, using either the "apply" operator or
    3.28    direct function application.*)
    3.29 -fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
    3.30 +fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
    3.31        let val c = if c = "equal" then "c_fequal" else c
    3.32            val nargs = min_arity_of cma c
    3.33            val args1 = List.take(args, nargs)
    3.34 @@ -232,21 +230,22 @@
    3.35                                           Int.toString nargs ^ " but is applied to " ^
    3.36                                           space_implode ", " args)
    3.37            val args2 = List.drop(args, nargs)
    3.38 -          val targs = if not t_full then map string_of_fol_type tvars else []
    3.39 +          val targs = if full_types then [] else map string_of_fol_type tvars
    3.40        in
    3.41            string_apply (c ^ paren_pack (args1@targs), args2)
    3.42        end
    3.43    | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
    3.44    | string_of_applic _ _ _ = error "string_of_applic";
    3.45  
    3.46 -fun wrap_type_if t_full cnh (head, s, tp) =
    3.47 -  if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
    3.48 +fun wrap_type_if full_types cnh (head, s, tp) =
    3.49 +  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
    3.50  
    3.51 -fun string_of_combterm (params as (t_full, cma, cnh)) t =
    3.52 +fun string_of_combterm (params as (full_types, cma, cnh)) t =
    3.53    let val (head, args) = strip_combterm_comb t
    3.54 -  in  wrap_type_if t_full cnh (head,
    3.55 -                    string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
    3.56 -                    type_of_combterm t)
    3.57 +  in  wrap_type_if full_types cnh (head,
    3.58 +          string_of_applic full_types cma
    3.59 +                           (head, map (string_of_combterm (params)) args),
    3.60 +          type_of_combterm t)
    3.61    end;
    3.62  
    3.63  (*Boolean-valued terms are here converted to literals.*)
    3.64 @@ -318,11 +317,11 @@
    3.65  
    3.66  fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
    3.67  
    3.68 -fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
    3.69 +fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
    3.70        if c = "equal" then (addtypes tvars funcs, preds)
    3.71        else
    3.72          let val arity = min_arity_of cma c
    3.73 -            val ntys = if not t_full then length tvars else 0
    3.74 +            val ntys = if not full_types then length tvars else 0
    3.75              val addit = Symtab.update(c, arity+ntys)
    3.76          in
    3.77              if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
    3.78 @@ -452,12 +451,12 @@
    3.79  
    3.80  (* TPTP format *)
    3.81  
    3.82 -fun write_tptp_file t_full file clauses =
    3.83 +fun write_tptp_file full_types file clauses =
    3.84    let
    3.85      val (conjectures, axclauses, _, helper_clauses,
    3.86        classrel_clauses, arity_clauses) = clauses
    3.87      val (cma, cnh) = count_constants clauses
    3.88 -    val params = (t_full, cma, cnh)
    3.89 +    val params = (full_types, cma, cnh)
    3.90      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    3.91      val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
    3.92      val _ =
    3.93 @@ -474,12 +473,12 @@
    3.94  
    3.95  (* DFG format *)
    3.96  
    3.97 -fun write_dfg_file t_full file clauses =
    3.98 +fun write_dfg_file full_types file clauses =
    3.99    let
   3.100      val (conjectures, axclauses, _, helper_clauses,
   3.101        classrel_clauses, arity_clauses) = clauses
   3.102      val (cma, cnh) = count_constants clauses
   3.103 -    val params = (t_full, cma, cnh)
   3.104 +    val params = (full_types, cma, cnh)
   3.105      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   3.106      and probname = Path.implode (Path.base file)
   3.107      val axstrs = map (#1 o (clause2dfg params)) axclauses
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 22 15:23:18 2010 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 23 11:39:21 2010 +0100
     4.3 @@ -4,43 +4,125 @@
     4.4  Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
     4.5  *)
     4.6  
     4.7 +signature SLEDGEHAMMER_ISAR =
     4.8 +sig
     4.9 +  type params = ATP_Manager.params
    4.10 +
    4.11 +  val default_params : theory -> (string * string) list -> params
    4.12 +end;
    4.13 +
    4.14  structure Sledgehammer_Isar : sig end =
    4.15  struct
    4.16  
    4.17  open ATP_Manager
    4.18  open ATP_Minimal
    4.19 +open Sledgehammer_Util
    4.20  
    4.21  structure K = OuterKeyword and P = OuterParse
    4.22  
    4.23 -val _ =
    4.24 -  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
    4.25 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
    4.26 +type raw_param = string * string list
    4.27 +
    4.28 +val default_default_params =
    4.29 +  [("debug", "false"),
    4.30 +   ("verbose", "false"),
    4.31 +   ("relevance_threshold", "0.5"),
    4.32 +   ("higher_order", "smart"),
    4.33 +   ("respect_no_atp", "true"),
    4.34 +   ("follow_defs", "false"),
    4.35 +   ("isar_proof", "false"),
    4.36 +   ("minimize_timeout", "5 s")]
    4.37 +
    4.38 +val negated_params =
    4.39 +  [("no_debug", "debug"),
    4.40 +   ("quiet", "verbose"),
    4.41 +   ("partial_types", "full_types"),
    4.42 +   ("first_order", "higher_order"),
    4.43 +   ("ignore_no_atp", "respect_no_atp"),
    4.44 +   ("dont_follow_defs", "follow_defs"),
    4.45 +   ("metis_proof", "isar_proof")]
    4.46 +
    4.47 +val property_affected_params = ["atps", "full_types", "timeout"]
    4.48  
    4.49 -val _ =
    4.50 -  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
    4.51 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
    4.52 +fun is_known_raw_param s =
    4.53 +  AList.defined (op =) default_default_params s orelse
    4.54 +  AList.defined (op =) negated_params s orelse
    4.55 +  member (op =) property_affected_params s
    4.56 +
    4.57 +fun check_raw_param (s, _) =
    4.58 +  if is_known_raw_param s then ()
    4.59 +  else error ("Unknown parameter: " ^ quote s ^ ".")
    4.60  
    4.61 -val _ =
    4.62 -  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
    4.63 -    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
    4.64 -      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
    4.65 +fun unnegate_raw_param (name, value) =
    4.66 +  case AList.lookup (op =) negated_params name of
    4.67 +    SOME name' => (name', case value of
    4.68 +                            ["false"] => ["true"]
    4.69 +                          | ["true"] => ["false"]
    4.70 +                          | [] => ["false"]
    4.71 +                          | _ => value)
    4.72 +  | NONE => (name, value)
    4.73 +
    4.74 +structure Data = Theory_Data(
    4.75 +  type T = raw_param list
    4.76 +  val empty = default_default_params |> map (apsnd single)
    4.77 +  val extend = I
    4.78 +  fun merge p : T = AList.merge (op =) (K true) p)
    4.79  
    4.80 -val _ =
    4.81 -  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
    4.82 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    4.83 -      Toplevel.keep (print_provers o Toplevel.theory_of)));
    4.84 +val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
    4.85 +fun default_raw_params thy =
    4.86 +  [("atps", [!atps]),
    4.87 +   ("full_types", [if !full_types then "true" else "false"]),
    4.88 +   ("timeout", [string_of_int (!timeout) ^ " s"])] @
    4.89 +  Data.get thy
    4.90 +
    4.91 +val infinity_time_in_secs = 60 * 60 * 24 * 365
    4.92 +val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
    4.93  
    4.94 -val _ =
    4.95 -  OuterSyntax.improper_command "sledgehammer"
    4.96 -    "search for first-order proof using automatic theorem provers" K.diag
    4.97 -    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
    4.98 -      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
    4.99 +fun extract_params thy default_params override_params =
   4.100 +  let
   4.101 +    val override_params = map unnegate_raw_param override_params
   4.102 +    val raw_params = rev override_params @ rev default_params
   4.103 +    val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
   4.104 +    val lookup_string = the_default "" o lookup
   4.105 +    fun general_lookup_bool option default_value name =
   4.106 +      case lookup name of
   4.107 +        SOME s => s |> parse_bool_option option name
   4.108 +      | NONE => default_value
   4.109 +    val lookup_bool = the o general_lookup_bool false (SOME false)
   4.110 +    val lookup_bool_option = general_lookup_bool true NONE
   4.111 +    fun lookup_time name =
   4.112 +      the_timeout (case lookup name of
   4.113 +                     NONE => NONE
   4.114 +                   | SOME s => parse_time_option name s)
   4.115 +    fun lookup_real name =
   4.116 +      case lookup name of
   4.117 +        NONE => 0.0
   4.118 +      | SOME s => 0.0 (* FIXME ### *)
   4.119 +    val debug = lookup_bool "debug"
   4.120 +    val verbose = debug orelse lookup_bool "verbose"
   4.121 +    val atps = lookup_string "atps" |> space_explode " "
   4.122 +    val full_types = lookup_bool "full_types"
   4.123 +    val relevance_threshold = lookup_real "relevance_threshold"
   4.124 +    val higher_order = lookup_bool_option "higher_order"
   4.125 +    val respect_no_atp = lookup_bool "respect_no_atp"
   4.126 +    val follow_defs = lookup_bool "follow_defs"
   4.127 +    val isar_proof = lookup_bool "isar_proof"
   4.128 +    val timeout = lookup_time "timeout"
   4.129 +    val minimize_timeout = lookup_time "minimize_timeout"
   4.130 +  in
   4.131 +    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
   4.132 +     relevance_threshold = relevance_threshold, higher_order = higher_order,
   4.133 +     respect_no_atp = respect_no_atp, follow_defs = follow_defs,
   4.134 +     isar_proof = isar_proof, timeout = timeout,
   4.135 +     minimize_timeout = minimize_timeout}
   4.136 +  end
   4.137  
   4.138 -val default_minimize_prover = "remote_vampire"
   4.139 -val default_minimize_time_limit = 5
   4.140 +fun default_params thy =
   4.141 +  extract_params thy (default_raw_params thy) o map (apsnd single)
   4.142  
   4.143  fun atp_minimize_command args thm_names state =
   4.144    let
   4.145 +    val thy = Proof.theory_of state
   4.146 +    val ctxt = Proof.context_of state
   4.147      fun theorems_from_names ctxt =
   4.148        map (fn (name, interval) =>
   4.149                let
   4.150 @@ -48,40 +130,104 @@
   4.151                  val ths = ProofContext.get_fact ctxt thmref
   4.152                  val name' = Facts.string_of_ref thmref
   4.153                in (name', ths) end)
   4.154 -    fun get_time_limit_arg time_string =
   4.155 -      (case Int.fromString time_string of
   4.156 -        SOME t => t
   4.157 -      | NONE => error ("Invalid time limit: " ^ quote time_string))
   4.158 +    fun get_time_limit_arg s =
   4.159 +      (case Int.fromString s of
   4.160 +        SOME t => Time.fromSeconds t
   4.161 +      | NONE => error ("Invalid time limit: " ^ quote s))
   4.162      fun get_opt (name, a) (p, t) =
   4.163        (case name of
   4.164          "time" => (p, get_time_limit_arg a)
   4.165        | "atp" => (a, t)
   4.166        | n => error ("Invalid argument: " ^ n))
   4.167 -    fun get_options args =
   4.168 -      fold get_opt args (default_minimize_prover, default_minimize_time_limit)
   4.169 -    val (prover_name, time_limit) = get_options args
   4.170 +    val {atps, minimize_timeout, ...} = default_params thy []
   4.171 +    fun get_options args = fold get_opt args (hd atps, minimize_timeout)
   4.172 +    val (atp, timeout) = get_options args
   4.173 +    val params =
   4.174 +      default_params thy
   4.175 +          [("atps", atp),
   4.176 +           ("minimize_timeout", string_of_int (Time.toSeconds timeout) ^ " s")]
   4.177      val prover =
   4.178 -      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
   4.179 +      (case get_prover thy atp of
   4.180          SOME prover => prover
   4.181 -      | NONE => error ("Unknown prover: " ^ quote prover_name))
   4.182 -    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
   4.183 +      | NONE => error ("Unknown ATP: " ^ quote atp))
   4.184 +    val name_thms_pairs = theorems_from_names ctxt thm_names
   4.185    in
   4.186 -    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
   4.187 -                                   state name_thms_pairs))
   4.188 +    writeln (#2 (minimize_theorems params linear_minimize prover atp state
   4.189 +                                   name_thms_pairs))
   4.190    end
   4.191  
   4.192 -local structure K = OuterKeyword and P = OuterParse in
   4.193 -
   4.194  val parse_args =
   4.195    Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
   4.196  val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
   4.197 -
   4.198  val _ =
   4.199 -  OuterSyntax.improper_command "atp_minimize" "minimize theorem list with external prover" K.diag
   4.200 +  OuterSyntax.improper_command "atp_minimize"
   4.201 +    "minimize theorem list with external prover" K.diag
   4.202      (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
   4.203        Toplevel.no_timing o Toplevel.unknown_proof o
   4.204          Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
   4.205  
   4.206 -end
   4.207 +fun hammer_away override_params i state =
   4.208 +  let
   4.209 +    val thy = Proof.theory_of state
   4.210 +    val _ = List.app check_raw_param override_params
   4.211 +    val params = extract_params thy (default_raw_params thy) override_params
   4.212 +  in sledgehammer params i state end
   4.213 +
   4.214 +fun sledgehammer_trans (opt_params, opt_i) =
   4.215 +  Toplevel.keep (hammer_away (these opt_params) (the_default 1 opt_i)
   4.216 +                 o Toplevel.proof_of)
   4.217 +
   4.218 +fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
   4.219 +
   4.220 +fun sledgehammer_params_trans opt_params =
   4.221 +  Toplevel.theory
   4.222 +      (fold set_default_raw_param (these opt_params)
   4.223 +       #> tap (fn thy => 
   4.224 +                  writeln ("Default parameters for Sledgehammer:\n" ^
   4.225 +                           (case rev (default_raw_params thy) of
   4.226 +                              [] => "none"
   4.227 +                            | params =>
   4.228 +                              (map check_raw_param params;
   4.229 +                               params |> map string_for_raw_param
   4.230 +                                      |> sort_strings |> cat_lines)))))
   4.231 +
   4.232 +val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
   4.233 +val parse_value =
   4.234 +  Scan.repeat1 (P.minus >> single
   4.235 +                || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat
   4.236 +val parse_param =
   4.237 +  parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these)
   4.238 +val parse_params =
   4.239 +  Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]")
   4.240 +val parse_sledgehammer_command =
   4.241 +  (parse_params -- Scan.option P.nat) #>> sledgehammer_trans
   4.242 +val parse_sledgehammer_params_command =
   4.243 +  parse_params #>> sledgehammer_params_trans
   4.244 +
   4.245 +val _ =
   4.246 +  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   4.247 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill))
   4.248 +val _ =
   4.249 +  OuterSyntax.improper_command "atp_info"
   4.250 +    "print information about managed provers" K.diag
   4.251 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info))
   4.252 +val _ =
   4.253 +  OuterSyntax.improper_command "atp_messages"
   4.254 +    "print recent messages issued by managed provers" K.diag
   4.255 +    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   4.256 +      (fn limit => Toplevel.no_timing
   4.257 +                   o Toplevel.imperative (fn () => messages limit)))
   4.258 +val _ =
   4.259 +  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   4.260 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   4.261 +      Toplevel.keep (print_provers o Toplevel.theory_of)))
   4.262 +val _ =
   4.263 +  OuterSyntax.improper_command "sledgehammer"
   4.264 +    "search for first-order proof using automatic theorem provers" K.diag
   4.265 +    parse_sledgehammer_command
   4.266 +val _ =
   4.267 +  OuterSyntax.command "sledgehammer_params"
   4.268 +    "set and display the default parameters for Sledgehammer" K.thy_decl
   4.269 +    parse_sledgehammer_params_command
   4.270  
   4.271  end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 22 15:23:18 2010 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Mar 23 11:39:21 2010 +0100
     5.3 @@ -540,9 +540,10 @@
     5.4  
     5.5  (* atp_minimize [atp=<prover>] <lemmas> *)
     5.6  fun minimize_line _ [] = ""
     5.7 -  | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
     5.8 -        Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
     5.9 -                                       space_implode " " (kill_chained lemmas))
    5.10 +  | minimize_line name lemmas =
    5.11 +      "To minimize the number of lemmas, try this command:\n" ^
    5.12 +      Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
    5.13 +                                     space_implode " " (kill_chained lemmas))
    5.14  
    5.15  fun metis_lemma_list dfg name result =
    5.16    let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
    5.17 @@ -570,8 +571,11 @@
    5.18        if member (op =) tokens chained_hint then ""
    5.19        else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
    5.20    in
    5.21 -    (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
    5.22 -     lemma_names)
    5.23 +    (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
    5.24 +       for a strange ProofGeneral bug, whereby the first two letters of the word
    5.25 +       "proof" are not highlighted. *)
    5.26 +    (one_line_proof ^ "\n\nStructured proof:" ^
    5.27 +     Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
    5.28    end
    5.29  
    5.30  end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Mar 23 11:39:21 2010 +0100
     6.3 @@ -0,0 +1,53 @@
     6.4 +(*  Title:      HOL/Sledgehammer/sledgehammer_util.ML
     6.5 +    Author:     Jasmin Blanchette, TU Muenchen
     6.6 +
     6.7 +General-purpose functions used by the Sledgehammer modules.
     6.8 +*)
     6.9 +
    6.10 +signature SLEDGEHAMMER_UTIL =
    6.11 +sig
    6.12 +  val serial_commas : string -> string list -> string list
    6.13 +  val parse_bool_option : bool -> string -> string -> bool option
    6.14 +  val parse_time_option : string -> string -> Time.time option
    6.15 +end;
    6.16 +
    6.17 +structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    6.18 +struct
    6.19 +
    6.20 +fun serial_commas _ [] = ["??"]
    6.21 +  | serial_commas _ [s] = [s]
    6.22 +  | serial_commas conj [s1, s2] = [s1, conj, s2]
    6.23 +  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    6.24 +  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    6.25 +
    6.26 +fun parse_bool_option option name s =
    6.27 +  (case s of
    6.28 +     "smart" => if option then NONE else raise Option
    6.29 +   | "false" => SOME false
    6.30 +   | "true" => SOME true
    6.31 +   | "" => SOME true
    6.32 +   | _ => raise Option)
    6.33 +  handle Option.Option =>
    6.34 +         let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
    6.35 +           error ("Parameter " ^ quote name ^ " must be assigned " ^
    6.36 +                  space_implode " " (serial_commas "or" ss) ^ ".")
    6.37 +         end
    6.38 +
    6.39 +fun parse_time_option _ "none" = NONE
    6.40 +  | parse_time_option name s =
    6.41 +    let
    6.42 +      val msecs =
    6.43 +        case space_explode " " s of
    6.44 +          [s1, "min"] => 60000 * the (Int.fromString s1)
    6.45 +        | [s1, "s"] => 1000 * the (Int.fromString s1)
    6.46 +        | [s1, "ms"] => the (Int.fromString s1)
    6.47 +        | _ => 0
    6.48 +    in
    6.49 +      if msecs <= 0 then
    6.50 +        error ("Parameter " ^ quote name ^ " must be assigned a positive time \
    6.51 +               \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
    6.52 +      else
    6.53 +        SOME (Time.fromMilliseconds msecs)
    6.54 +    end
    6.55 +
    6.56 +end;