simplify MaSh term patterns + add missing global facts if there aren't too many
authorblanchet
Tue Dec 04 10:02:51 2012 +0100 (2012-12-04)
changeset 5034072519bf5f135
parent 50339 d8dae91f3107
child 50341 0c65a7cfc0f3
child 50342 e77b0dbcae5b
simplify MaSh term patterns + add missing global facts if there aren't too many
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 00:37:11 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 10:02:51 2012 +0100
     1.3 @@ -102,8 +102,7 @@
     1.4  val relearn_atpN = "relearn_atp"
     1.5  
     1.6  fun mash_model_dir () =
     1.7 -  Path.explode "$ISABELLE_HOME_USER/mash"
     1.8 -  |> tap Isabelle_System.mkdir
     1.9 +  Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
    1.10  val mash_state_dir = mash_model_dir
    1.11  fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
    1.12  
    1.13 @@ -496,7 +495,7 @@
    1.14          let
    1.15            val ps = patternify_term (u :: args) depth t
    1.16            val qs = "" :: patternify_term [] (depth - 1) u
    1.17 -        in map_product (fn p => fn q => p ^ "(" ^ q ^ ")") ps qs end
    1.18 +        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
    1.19        | patternify_term _ _ _ = []
    1.20      val add_term_pattern = union (op =) oo patternify_term []
    1.21      fun add_term_patterns ~1 _ = I
    1.22 @@ -670,6 +669,9 @@
    1.23    | interleave 1 (x :: _) _ = [x]
    1.24    | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
    1.25  
    1.26 +(* factor that controls whether unknown global facts should be included *)
    1.27 +val include_unk_global_factor = 15
    1.28 +
    1.29  fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    1.30                           concl_t facts =
    1.31    let
    1.32 @@ -698,9 +700,13 @@
    1.33      val (unk_global, unk_local) =
    1.34        unchained |> filter_out (is_fact_in_graph fact_G)
    1.35                  |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
    1.36 +    val (small_unk_global, big_unk_global) =
    1.37 +      ([], unk_global)
    1.38 +      |> include_unk_global_factor * length unk_global <= max_facts ? swap
    1.39    in
    1.40 -    (interleave max_facts (chained @ unk_local) sels |> weight_mepo_facts,
    1.41 -     unk_global)
    1.42 +    (interleave max_facts (chained @ unk_local @ small_unk_global) sels
    1.43 +     |> weight_mepo_facts (* use MePo weights for now *),
    1.44 +     big_unk_global)
    1.45    end
    1.46  
    1.47  fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
    1.48 @@ -931,21 +937,21 @@
    1.49        mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts
    1.50        |> Output.urgent_message
    1.51    in
    1.52 -    (if atp then
    1.53 -       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
    1.54 -        plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^
    1.55 -        string_from_time timeout ^ ").\n\nCollecting Isar proofs first..."
    1.56 -        |> Output.urgent_message;
    1.57 -        learn 1 false;
    1.58 -        "Now collecting ATP proofs. This may take several hours. You can \
    1.59 -        \safely stop the learning process at any point."
    1.60 -        |> Output.urgent_message;
    1.61 -        learn 0 true)
    1.62 -     else
    1.63 -       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
    1.64 -        plural_s num_facts ^ " for Isar proofs..."
    1.65 -        |> Output.urgent_message;
    1.66 -        learn 0 false))
    1.67 +    if atp then
    1.68 +      ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
    1.69 +       plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^
    1.70 +       string_from_time timeout ^ ").\n\nCollecting Isar proofs first..."
    1.71 +       |> Output.urgent_message;
    1.72 +       learn 1 false;
    1.73 +       "Now collecting ATP proofs. This may take several hours. You can \
    1.74 +       \safely stop the learning process at any point."
    1.75 +       |> Output.urgent_message;
    1.76 +       learn 0 true)
    1.77 +    else
    1.78 +      ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
    1.79 +       plural_s num_facts ^ " for Isar proofs..."
    1.80 +       |> Output.urgent_message;
    1.81 +       learn 0 false)
    1.82    end
    1.83  
    1.84  fun is_mash_enabled () = (getenv "MASH" = "yes")