renamed options
authorblanchet
Fri May 14 22:29:50 2010 +0200 (2010-05-14)
changeset 36924ff01d3ae9ad4
parent 36923 538cf3fdfe4d
child 36925 ffad77bb3046
renamed options
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri May 14 22:28:39 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri May 14 22:29:50 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4       theory_relevant: bool option,
     1.5       defs_relevant: bool,
     1.6       isar_proof: bool,
     1.7 -     shrink_factor: int,
     1.8 +     isar_shrink_factor: int,
     1.9       timeout: Time.time,
    1.10       minimize_timeout: Time.time}
    1.11    type problem =
    1.12 @@ -83,7 +83,7 @@
    1.13     theory_relevant: bool option,
    1.14     defs_relevant: bool,
    1.15     isar_proof: bool,
    1.16 -   shrink_factor: int,
    1.17 +   isar_shrink_factor: int,
    1.18     timeout: Time.time,
    1.19     minimize_timeout: Time.time}
    1.20  
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri May 14 22:28:39 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri May 14 22:29:50 2010 +0200
     2.3 @@ -112,8 +112,8 @@
     2.4  
     2.5  fun generic_prover overlord get_facts prepare write_file home_var executable
     2.6          args proof_delims known_failures name
     2.7 -        ({debug, full_types, explicit_apply, isar_proof, shrink_factor, ...}
     2.8 -         : params) minimize_command
     2.9 +        ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
    2.10 +         ...} : params) minimize_command
    2.11          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    2.12           : problem) =
    2.13    let
    2.14 @@ -218,7 +218,8 @@
    2.15        case outcome of
    2.16          NONE =>
    2.17          proof_text isar_proof
    2.18 -            (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
    2.19 +            (pool, debug, full_types, isar_shrink_factor, ctxt,
    2.20 +             conjecture_shape)
    2.21              (minimize_command, proof, internal_thm_names, th, subgoal)
    2.22        | SOME failure => (string_for_failure failure ^ "\n", [])
    2.23    in
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri May 14 22:28:39 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri May 14 22:29:50 2010 +0200
     3.3 @@ -69,7 +69,7 @@
     3.4  (* minimalization of thms *)
     3.5  
     3.6  fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
     3.7 -                                  isar_proof, shrink_factor, ...})
     3.8 +                                  isar_proof, isar_shrink_factor, ...})
     3.9                        i n state name_thms_pairs =
    3.10    let
    3.11      val thy = Proof.theory_of state
    3.12 @@ -110,7 +110,8 @@
    3.13          in
    3.14            (SOME min_thms,
    3.15             proof_text isar_proof
    3.16 -               (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
    3.17 +               (pool, debug, full_types, isar_shrink_factor, ctxt,
    3.18 +                conjecture_shape)
    3.19                 (K "", proof, internal_thm_names, goal, i) |> fst)
    3.20          end
    3.21      | {outcome = SOME TimedOut, ...} =>
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 22:28:39 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 22:29:50 2010 +0200
     4.3 @@ -98,7 +98,7 @@
     4.4     ("theory_relevant", "smart"),
     4.5     ("defs_relevant", "false"),
     4.6     ("isar_proof", "false"),
     4.7 -   ("shrink_factor", "1"),
     4.8 +   ("isar_shrink_factor", "1"),
     4.9     ("minimize_timeout", "5 s")]
    4.10  
    4.11  val alias_params =
    4.12 @@ -116,7 +116,7 @@
    4.13  
    4.14  val params_for_minimize =
    4.15    ["debug", "verbose", "overlord", "full_types", "explicit_apply",
    4.16 -   "isar_proof", "shrink_factor", "minimize_timeout"]
    4.17 +   "isar_proof", "isar_shrink_factor", "minimize_timeout"]
    4.18  
    4.19  val property_dependent_params = ["atps", "full_types", "timeout"]
    4.20  
    4.21 @@ -199,7 +199,7 @@
    4.22      val theory_relevant = lookup_bool_option "theory_relevant"
    4.23      val defs_relevant = lookup_bool "defs_relevant"
    4.24      val isar_proof = lookup_bool "isar_proof"
    4.25 -    val shrink_factor = Int.max (1, lookup_int "shrink_factor")
    4.26 +    val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    4.27      val timeout = lookup_time "timeout"
    4.28      val minimize_timeout = lookup_time "minimize_timeout"
    4.29    in
    4.30 @@ -208,8 +208,8 @@
    4.31       respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    4.32       relevance_convergence = relevance_convergence,
    4.33       theory_relevant = theory_relevant, defs_relevant = defs_relevant,
    4.34 -     isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout,
    4.35 -     minimize_timeout = minimize_timeout}
    4.36 +     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    4.37 +     timeout = timeout, minimize_timeout = minimize_timeout}
    4.38    end
    4.39  
    4.40  fun get_params thy = extract_params thy (default_raw_params thy)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri May 14 22:28:39 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri May 14 22:29:50 2010 +0200
     5.3 @@ -569,7 +569,7 @@
     5.4  
     5.5  fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
     5.6      (j, line :: lines)
     5.7 -  | add_desired_line ctxt shrink_factor conjecture_shape thm_names frees
     5.8 +  | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
     5.9                       (Inference (num, t, deps)) (j, lines) =
    5.10      (j + 1,
    5.11       if is_axiom_clause_number thm_names num orelse
    5.12 @@ -579,7 +579,7 @@
    5.13           not (exists_subterm (is_bad_free frees) t) andalso
    5.14           not (is_trivial_formula t) andalso
    5.15           (null lines orelse (* last line must be kept *)
    5.16 -          (length deps >= 2 andalso j mod shrink_factor = 0))) then
    5.17 +          (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
    5.18         Inference (num, t, deps) :: lines  (* keep line *)
    5.19       else
    5.20         map (replace_deps_in_line (num, deps)) lines)  (* drop line *)
    5.21 @@ -674,7 +674,7 @@
    5.22            forall_vars t,
    5.23            ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
    5.24  
    5.25 -fun proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof
    5.26 +fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
    5.27                           conjecture_shape thm_names params frees =
    5.28    let
    5.29      val lines =
    5.30 @@ -683,7 +683,7 @@
    5.31        |> decode_lines ctxt full_types
    5.32        |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
    5.33        |> rpair [] |-> fold_rev add_nontrivial_line
    5.34 -      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor
    5.35 +      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
    5.36                                                 conjecture_shape thm_names frees)
    5.37        |> snd
    5.38    in
    5.39 @@ -981,7 +981,7 @@
    5.40          do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
    5.41    in do_proof end
    5.42  
    5.43 -fun isar_proof_text (pool, debug, full_types, shrink_factor, ctxt,
    5.44 +fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
    5.45                       conjecture_shape)
    5.46                      (minimize_command, atp_proof, thm_names, goal, i) =
    5.47    let
    5.48 @@ -992,8 +992,9 @@
    5.49      val (one_line_proof, lemma_names) =
    5.50        metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
    5.51      fun isar_proof_for () =
    5.52 -      case proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof
    5.53 -                                conjecture_shape thm_names params frees
    5.54 +      case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
    5.55 +                                atp_proof conjecture_shape thm_names params
    5.56 +                                frees
    5.57             |> redirect_proof thy conjecture_shape hyp_ts concl_t
    5.58             |> kill_duplicate_assumptions_in_proof
    5.59             |> then_chain_proof