added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
authorblanchet
Tue Apr 20 16:04:36 2010 +0200 (2010-04-20)
changeset 3623561159615a0c5
parent 36234 77abfa526524
child 36236 5563c717638a
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 20 14:39:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 20 16:04:36 2010 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4       overlord: bool,
     1.5       atps: string list,
     1.6       full_types: bool,
     1.7 +     explicit_apply: bool,
     1.8       respect_no_atp: bool,
     1.9       relevance_threshold: real,
    1.10       convergence: real,
    1.11 @@ -69,6 +70,7 @@
    1.12     overlord: bool,
    1.13     atps: string list,
    1.14     full_types: bool,
    1.15 +   explicit_apply: bool,
    1.16     respect_no_atp: bool,
    1.17     relevance_threshold: real,
    1.18     convergence: real,
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Apr 20 14:39:42 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Apr 20 16:04:36 2010 +0200
     2.3 @@ -67,7 +67,7 @@
     2.4    | (failure :: _) => SOME failure
     2.5  
     2.6  fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
     2.7 -        proof_text name ({debug, full_types, ...} : params)
     2.8 +        proof_text name ({debug, full_types, explicit_apply, ...} : params)
     2.9          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    2.10           : problem) =
    2.11    let
    2.12 @@ -128,7 +128,7 @@
    2.13        if Config.get ctxt measure_runtime then split_time s else (s, 0)
    2.14      fun run_on probfile =
    2.15        if File.exists cmd then
    2.16 -        write_file full_types probfile clauses
    2.17 +        write_file full_types explicit_apply probfile clauses
    2.18          |> pair (apfst split_time' (bash_output (cmd_line probfile)))
    2.19        else error ("Bad executable: " ^ Path.implode cmd ^ ".");
    2.20  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 14:39:42 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 16:04:36 2010 +0200
     3.3 @@ -34,10 +34,10 @@
     3.4    val get_helper_clauses : bool -> theory -> bool ->
     3.5         hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
     3.6         hol_clause list
     3.7 -  val write_tptp_file : bool -> bool -> Path.T ->
     3.8 +  val write_tptp_file : bool -> bool -> bool -> Path.T ->
     3.9      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    3.10      classrel_clause list * arity_clause list -> unit
    3.11 -  val write_dfg_file : bool -> Path.T ->
    3.12 +  val write_dfg_file : bool -> bool -> Path.T ->
    3.13      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    3.14      classrel_clause list * arity_clause list -> unit
    3.15  end
    3.16 @@ -50,19 +50,19 @@
    3.17  open Sledgehammer_Fact_Preprocessor
    3.18  
    3.19  (* Parameter "full_types" below indicates that full type information is to be
    3.20 -exported *)
    3.21 +   exported.
    3.22  
    3.23 -(* If true, each function will be directly applied to as many arguments as
    3.24 -   possible, avoiding use of the "apply" operator. Use of hBOOL is also
    3.25 -   minimized. *)
    3.26 -val minimize_applies = true;
    3.27 +   If "explicit_apply" is false, each function will be directly applied to as
    3.28 +   many arguments as possible, avoiding use of the "apply" operator. Use of
    3.29 +   hBOOL is also minimized.
    3.30 +*)
    3.31  
    3.32  fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
    3.33  
    3.34  (*True if the constant ever appears outside of the top-level position in literals.
    3.35    If false, the constant always receives all of its arguments and is used as a predicate.*)
    3.36 -fun needs_hBOOL const_needs_hBOOL c =
    3.37 -  not minimize_applies orelse
    3.38 +fun needs_hBOOL explicit_apply const_needs_hBOOL c =
    3.39 +  explicit_apply orelse
    3.40      the_default false (Symtab.lookup const_needs_hBOOL c);
    3.41  
    3.42  
    3.43 @@ -211,9 +211,10 @@
    3.44  
    3.45  val type_wrapper = "ti";
    3.46  
    3.47 -fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
    3.48 -    needs_hBOOL const_needs_hBOOL c
    3.49 -  | head_needs_hBOOL _ _ = true;
    3.50 +fun head_needs_hBOOL explicit_apply const_needs_hBOOL
    3.51 +                     (CombConst ((c, _), _, _)) =
    3.52 +    needs_hBOOL explicit_apply const_needs_hBOOL c
    3.53 +  | head_needs_hBOOL _ _ _ = true
    3.54  
    3.55  fun wrap_type full_types (s, ty) pool =
    3.56    if full_types then
    3.57 @@ -223,8 +224,11 @@
    3.58    else
    3.59      (s, pool)
    3.60  
    3.61 -fun wrap_type_if full_types cnh (head, s, tp) =
    3.62 -  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
    3.63 +fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
    3.64 +  if head_needs_hBOOL explicit_apply cnh head then
    3.65 +    wrap_type full_types (s, tp)
    3.66 +  else
    3.67 +    pair s
    3.68  
    3.69  fun apply ss = "hAPP" ^ paren_pack ss;
    3.70  
    3.71 @@ -252,18 +256,22 @@
    3.72    | string_of_application _ _ (CombVar (name, _), args) pool =
    3.73      nice_name name pool |>> (fn s => string_apply (s, args))
    3.74  
    3.75 -fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
    3.76 +fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
    3.77 +                       pool =
    3.78    let
    3.79      val (head, args) = strip_combterm_comb t
    3.80      val (ss, pool) = pool_map (string_of_combterm params) args pool
    3.81      val (s, pool) = string_of_application full_types cma (head, ss) pool
    3.82 -  in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
    3.83 +  in
    3.84 +    wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
    3.85 +                 pool
    3.86 +  end
    3.87  
    3.88  (*Boolean-valued terms are here converted to literals.*)
    3.89  fun boolify params c =
    3.90    string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
    3.91  
    3.92 -fun string_of_predicate (params as (_, _, cnh)) t =
    3.93 +fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
    3.94    case t of
    3.95      (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
    3.96      (* DFG only: new TPTP prefers infix equality *)
    3.97 @@ -272,7 +280,8 @@
    3.98    | _ =>
    3.99      case #1 (strip_combterm_comb t) of
   3.100        CombConst ((s, _), _, _) =>
   3.101 -      (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
   3.102 +      (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   3.103 +          params t
   3.104      | _ => boolify params t
   3.105  
   3.106  
   3.107 @@ -342,8 +351,8 @@
   3.108  
   3.109  fun add_types tvars = fold add_fol_type_funcs tvars
   3.110  
   3.111 -fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars))
   3.112 -              (funcs, preds) =
   3.113 +fun add_decls (full_types, explicit_apply, cma, cnh)
   3.114 +              (CombConst ((c, _), _, tvars)) (funcs, preds) =
   3.115        if c = "equal" then
   3.116          (add_types tvars funcs, preds)
   3.117        else
   3.118 @@ -351,8 +360,10 @@
   3.119              val ntys = if not full_types then length tvars else 0
   3.120              val addit = Symtab.update(c, arity+ntys)
   3.121          in
   3.122 -            if needs_hBOOL cnh c then (add_types tvars (addit funcs), preds)
   3.123 -            else (add_types tvars funcs, addit preds)
   3.124 +            if needs_hBOOL explicit_apply cnh c then
   3.125 +              (add_types tvars (addit funcs), preds)
   3.126 +            else
   3.127 +              (add_types tvars funcs, addit preds)
   3.128          end
   3.129    | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
   3.130        (add_fol_type_funcs ctp funcs, preds)
   3.131 @@ -458,18 +469,23 @@
   3.132                             (const_min_arity, const_needs_hBOOL) =
   3.133    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   3.134  
   3.135 -fun display_arity const_needs_hBOOL (c,n) =
   3.136 +fun display_arity explicit_apply const_needs_hBOOL (c,n) =
   3.137    trace_msg (fn () => "Constant: " ^ c ^
   3.138                  " arity:\t" ^ Int.toString n ^
   3.139 -                (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
   3.140 +                (if needs_hBOOL explicit_apply const_needs_hBOOL c then
   3.141 +                   " needs hBOOL"
   3.142 +                 else
   3.143 +                   ""))
   3.144  
   3.145 -fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   3.146 -  if minimize_applies then
   3.147 +fun count_constants explicit_apply
   3.148 +                    (conjectures, _, extra_clauses, helper_clauses, _, _) =
   3.149 +  if not explicit_apply then
   3.150       let val (const_min_arity, const_needs_hBOOL) =
   3.151            fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
   3.152         |> fold count_constants_clause extra_clauses
   3.153         |> fold count_constants_clause helper_clauses
   3.154 -     val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
   3.155 +     val _ = List.app (display_arity explicit_apply const_needs_hBOOL)
   3.156 +                      (Symtab.dest (const_min_arity))
   3.157       in (const_min_arity, const_needs_hBOOL) end
   3.158    else (Symtab.empty, Symtab.empty);
   3.159  
   3.160 @@ -479,15 +495,15 @@
   3.161  
   3.162  (* TPTP format *)
   3.163  
   3.164 -fun write_tptp_file readable_names full_types file clauses =
   3.165 +fun write_tptp_file readable_names full_types explicit_apply file clauses =
   3.166    let
   3.167      fun section _ [] = []
   3.168        | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
   3.169      val pool = empty_name_pool readable_names
   3.170      val (conjectures, axclauses, _, helper_clauses,
   3.171        classrel_clauses, arity_clauses) = clauses
   3.172 -    val (cma, cnh) = count_constants clauses
   3.173 -    val params = (full_types, cma, cnh)
   3.174 +    val (cma, cnh) = count_constants explicit_apply clauses
   3.175 +    val params = (full_types, explicit_apply, cma, cnh)
   3.176      val ((conjecture_clss, tfree_litss), pool) =
   3.177        pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   3.178      val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
   3.179 @@ -511,7 +527,7 @@
   3.180  
   3.181  (* DFG format *)
   3.182  
   3.183 -fun write_dfg_file full_types file clauses =
   3.184 +fun write_dfg_file full_types explicit_apply file clauses =
   3.185    let
   3.186      (* Some of the helper functions below are not name-pool-aware. However,
   3.187         there's no point in adding name pool support if the DFG format is on its
   3.188 @@ -519,8 +535,8 @@
   3.189      val pool = NONE
   3.190      val (conjectures, axclauses, _, helper_clauses,
   3.191        classrel_clauses, arity_clauses) = clauses
   3.192 -    val (cma, cnh) = count_constants clauses
   3.193 -    val params = (full_types, cma, cnh)
   3.194 +    val (cma, cnh) = count_constants explicit_apply clauses
   3.195 +    val params = (full_types, explicit_apply, cma, cnh)
   3.196      val ((conjecture_clss, tfree_litss), pool) =
   3.197        pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
   3.198      and probname = Path.implode (Path.base file)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 20 14:39:42 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 20 16:04:36 2010 +0200
     4.3 @@ -41,6 +41,7 @@
     4.4    [("debug", "false"),
     4.5     ("verbose", "false"),
     4.6     ("overlord", "false"),
     4.7 +   ("explicit_apply", "false"),
     4.8     ("respect_no_atp", "true"),
     4.9     ("relevance_threshold", "50"),
    4.10     ("convergence", "320"),
    4.11 @@ -58,6 +59,7 @@
    4.12    [("no_debug", "debug"),
    4.13     ("quiet", "verbose"),
    4.14     ("no_overlord", "overlord"),
    4.15 +   ("implicit_apply", "explicit_apply"),
    4.16     ("ignore_no_atp", "respect_no_atp"),
    4.17     ("partial_types", "full_types"),
    4.18     ("theory_irrelevant", "theory_relevant"),
    4.19 @@ -146,6 +148,7 @@
    4.20      val overlord = lookup_bool "overlord"
    4.21      val atps = lookup_string "atps" |> space_explode " "
    4.22      val full_types = lookup_bool "full_types"
    4.23 +    val explicit_apply = lookup_bool "explicit_apply"
    4.24      val respect_no_atp = lookup_bool "respect_no_atp"
    4.25      val relevance_threshold =
    4.26        0.01 * Real.fromInt (lookup_int "relevance_threshold")
    4.27 @@ -160,11 +163,12 @@
    4.28      val minimize_timeout = lookup_time "minimize_timeout"
    4.29    in
    4.30      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    4.31 -     full_types = full_types, respect_no_atp = respect_no_atp,
    4.32 -     relevance_threshold = relevance_threshold, convergence = convergence,
    4.33 -     theory_relevant = theory_relevant, higher_order = higher_order,
    4.34 -     follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
    4.35 -     sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
    4.36 +     full_types = full_types, explicit_apply = explicit_apply,
    4.37 +     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    4.38 +     convergence = convergence, theory_relevant = theory_relevant,
    4.39 +     higher_order = higher_order, follow_defs = follow_defs,
    4.40 +     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
    4.41 +     timeout = timeout, minimize_timeout = minimize_timeout}
    4.42    end
    4.43  
    4.44  fun get_params thy = extract_params thy (default_raw_params thy)