tuned ML function names
authorblanchet
Fri Jan 31 16:26:43 2014 +0100 (2014-01-31 ago)
changeset 55213dcb36a2540bc
parent 55212 5832470d956e
child 55214 48a347b40629
tuned ML function names
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:10:39 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:26:43 2014 +0100
     1.3 @@ -352,35 +352,35 @@
     1.4            |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
     1.5  *)
     1.6            |> isar_proof true params assms lems
     1.7 -          |> postprocess_remove_unreferenced_steps I
     1.8 -          |> relabel_proof_canonically
     1.9 -          |> `(proof_preplay_data debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.10 -               preplay_timeout)
    1.11 +          |> postprocess_isar_proof_remove_unreferenced_steps I
    1.12 +          |> relabel_isar_proof_canonically
    1.13 +          |> `(preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.14 +                 preplay_timeout)
    1.15  
    1.16          val (play_outcome, isar_proof) =
    1.17            isar_proof
    1.18 -          |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0) preplay_data
    1.19 +          |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
    1.20 +               preplay_data
    1.21            |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
    1.22 -          |> postprocess_remove_unreferenced_steps (try0_isar ? minimal_deps_of_step preplay_data)
    1.23 +          |> postprocess_isar_proof_remove_unreferenced_steps
    1.24 +               (try0_isar ? minimize_isar_step_dependencies preplay_data)
    1.25            |> `overall_preplay_outcome
    1.26            ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
    1.27  
    1.28          val isar_text =
    1.29 -          string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
    1.30 +          string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
    1.31        in
    1.32          (case isar_text of
    1.33            "" =>
    1.34 -          if isar_proofs = SOME true then
    1.35 -            "\nNo structured proof available (proof too simple)."
    1.36 -          else
    1.37 -            ""
    1.38 +          if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
    1.39 +          else ""
    1.40          | _ =>
    1.41            let
    1.42              val msg =
    1.43                (if verbose then
    1.44 -                let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
    1.45 -                  [string_of_int num_steps ^ " step" ^ plural_s num_steps]
    1.46 -                end
    1.47 +                 let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
    1.48 +                   [string_of_int num_steps ^ " step" ^ plural_s num_steps]
    1.49 +                 end
    1.50                 else
    1.51                   []) @
    1.52                (if do_preplay then [string_of_play_outcome play_outcome] else [])
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:10:39 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:26:43 2014 +0100
     2.3 @@ -9,12 +9,12 @@
     2.4  When configuring the pretty printer appropriately, the constraints will show up as type annotations
     2.5  when printing the term. This allows the term to be printed and reparsed without a change of types.
     2.6  
     2.7 -NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax.
     2.8 +Note: Terms should be unchecked before calling "annotate_types_in_term" to avoid awkward syntax.
     2.9  *)
    2.10  
    2.11  signature SLEDGEHAMMER_ISAR_ANNOTATE =
    2.12  sig
    2.13 -  val annotate_types : Proof.context -> term -> term
    2.14 +  val annotate_types_in_term : Proof.context -> term -> term
    2.15  end;
    2.16  
    2.17  structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE =
    2.18 @@ -197,7 +197,7 @@
    2.19    end
    2.20  
    2.21  (* (7) Annotate *)
    2.22 -fun annotate_types ctxt t =
    2.23 +fun annotate_types_in_term ctxt t =
    2.24    let
    2.25      val t' = generalize_types ctxt t
    2.26      val subst = match_types ctxt t' t
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 16:10:39 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 16:26:43 2014 +0100
     3.3 @@ -9,9 +9,9 @@
     3.4  signature SLEDGEHAMMER_ISAR_COMPRESS =
     3.5  sig
     3.6    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
     3.7 -  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
     3.8 +  type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
     3.9  
    3.10 -  val compress_proof : real -> preplay_data -> isar_proof -> isar_proof
    3.11 +  val compress_isar_proof : real -> isar_preplay_data -> isar_proof -> isar_proof
    3.12  end;
    3.13  
    3.14  structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
    3.15 @@ -95,8 +95,8 @@
    3.16  
    3.17  (* Precondition: The proof must be labeled canonically
    3.18     (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
    3.19 -fun compress_proof compress_isar
    3.20 -    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data) proof =
    3.21 +fun compress_isar_proof compress_isar
    3.22 +    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
    3.23    if compress_isar <= 1.0 then
    3.24      proof
    3.25    else
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 16:10:39 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 16:26:43 2014 +0100
     4.3 @@ -7,12 +7,13 @@
     4.4  
     4.5  signature SLEDGEHAMMER_ISAR_MINIMIZE =
     4.6  sig
     4.7 -  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
     4.8    type isar_step = Sledgehammer_Isar_Proof.isar_step
     4.9    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    4.10 +  type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
    4.11  
    4.12 -  val minimal_deps_of_step : preplay_data -> isar_step -> isar_step
    4.13 -  val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
    4.14 +  val minimize_isar_step_dependencies : isar_preplay_data -> isar_step -> isar_step
    4.15 +  val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
    4.16 +    isar_proof
    4.17  end;
    4.18  
    4.19  structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
    4.20 @@ -24,8 +25,8 @@
    4.21  
    4.22  val slack = seconds 0.1
    4.23  
    4.24 -fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step
    4.25 -  | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
    4.26 +fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
    4.27 +  | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
    4.28        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
    4.29      (case get_preplay_outcome l of
    4.30        Played time =>
    4.31 @@ -46,7 +47,7 @@
    4.32        end
    4.33      | _ => step (* don't touch steps that time out or fail *))
    4.34  
    4.35 -fun postprocess_remove_unreferenced_steps postproc_step =
    4.36 +fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
    4.37    let
    4.38      val add_lfs = fold (Ord_List.insert label_ord)
    4.39  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 16:10:39 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 16:26:43 2014 +0100
     5.3 @@ -14,14 +14,14 @@
     5.4  
     5.5    val trace : bool Config.T
     5.6  
     5.7 -  type preplay_data =
     5.8 +  type isar_preplay_data =
     5.9      {get_preplay_outcome: label -> play_outcome,
    5.10       set_preplay_outcome: label -> play_outcome -> unit,
    5.11       preplay_quietly: Time.time -> isar_step -> play_outcome,
    5.12       overall_preplay_outcome: isar_proof -> play_outcome}
    5.13  
    5.14 -  val proof_preplay_data : bool -> Proof.context -> string -> string -> bool -> Time.time ->
    5.15 -    isar_proof -> preplay_data
    5.16 +  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
    5.17 +    isar_proof -> isar_preplay_data
    5.18  end;
    5.19  
    5.20  structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
    5.21 @@ -147,7 +147,7 @@
    5.22  
    5.23  (*** proof preplay interface ***)
    5.24  
    5.25 -type preplay_data =
    5.26 +type isar_preplay_data =
    5.27    {get_preplay_outcome: label -> play_outcome,
    5.28     set_preplay_outcome: label -> play_outcome -> unit,
    5.29     preplay_quietly: Time.time -> isar_step -> play_outcome,
    5.30 @@ -184,14 +184,14 @@
    5.31     calculation.
    5.32  
    5.33     Precondition: The proof must be labeled canonically; cf.
    5.34 -   "Slegehammer_Proof.relabel_proof_canonically". *)
    5.35 -fun proof_preplay_data debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    5.36 +   "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
    5.37 +fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    5.38    if not do_preplay then
    5.39      (* the "dont_preplay" option pretends that everything works just fine *)
    5.40      {get_preplay_outcome = K (Played Time.zeroTime),
    5.41       set_preplay_outcome = K (K ()),
    5.42       preplay_quietly = K (K (Played Time.zeroTime)),
    5.43 -     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_data
    5.44 +     overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
    5.45    else
    5.46      let
    5.47        val ctxt = enrich_context_with_local_facts proof ctxt
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:10:39 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:26:43 2014 +0100
     6.3 @@ -40,11 +40,10 @@
     6.4  
     6.5    structure Canonical_Label_Tab : TABLE
     6.6  
     6.7 -  (** canonical proof labels: 1, 2, 3, ... in postorder **)
     6.8    val canonical_label_ord : (label * label) -> order
     6.9 -  val relabel_proof_canonically : isar_proof -> isar_proof
    6.10 +  val relabel_isar_proof_canonically : isar_proof -> isar_proof
    6.11  
    6.12 -  val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
    6.13 +  val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
    6.14  end;
    6.15  
    6.16  structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    6.17 @@ -112,14 +111,14 @@
    6.18    type key = label
    6.19    val ord = canonical_label_ord)
    6.20  
    6.21 -fun relabel_proof_canonically proof =
    6.22 +fun relabel_isar_proof_canonically proof =
    6.23    let
    6.24      fun next_label l (next, subst) =
    6.25        let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
    6.26  
    6.27      fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
    6.28      handle Option.Option =>
    6.29 -      raise Fail "Sledgehammer_Isar_Proof: relabel_proof_canonically"
    6.30 +      raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
    6.31  
    6.32      fun do_assm (l, t) state =
    6.33        let
    6.34 @@ -149,7 +148,7 @@
    6.35  
    6.36  val indent_size = 2
    6.37  
    6.38 -fun string_of_proof ctxt type_enc lam_trans i n proof =
    6.39 +fun string_of_isar_proof ctxt type_enc lam_trans i n proof =
    6.40    let
    6.41      (* Make sure only type constraints inserted by the type annotation code are printed. *)
    6.42      val ctxt =
    6.43 @@ -183,7 +182,7 @@
    6.44      fun add_term term (s, ctxt) =
    6.45        (s ^ (term
    6.46              |> singleton (Syntax.uncheck_terms ctxt)
    6.47 -            |> annotate_types ctxt
    6.48 +            |> annotate_types_in_term ctxt
    6.49              |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
    6.50              |> simplify_spaces
    6.51              |> maybe_quote),
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 16:10:39 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 16:26:43 2014 +0100
     7.3 @@ -9,9 +9,9 @@
     7.4  signature SLEDGEHAMMER_ISAR_TRY0 =
     7.5  sig
     7.6    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
     7.7 -  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
     7.8 +  type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
     7.9  
    7.10 -  val try0_isar_proof : Time.time -> preplay_data -> isar_proof -> isar_proof
    7.11 +  val try0_isar_proof : Time.time -> isar_preplay_data -> isar_proof -> isar_proof
    7.12  end;
    7.13  
    7.14  structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
    7.15 @@ -30,7 +30,7 @@
    7.16  
    7.17  fun try0_step _ _ (step as Let _) = step
    7.18    | try0_step preplay_timeout
    7.19 -      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data)
    7.20 +      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
    7.21        (step as Prove (_, _, l, _, _, _)) =
    7.22      let
    7.23        val timeout =