# HG changeset patch # User blanchet # Date 1356725019 -3600 # Node ID 12c097ff32414cc8ae65b1c314bfb6b0b2785b0a # Parent b69079c146657882094c5075b460b9a7bceab9f0 slightly more elegant naming convention (to keep low-level and high-level APIs separated) diff -r b69079c14665 -r 12c097ff3241 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 28 14:13:39 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 28 21:03:39 2012 +0100 @@ -30,15 +30,20 @@ val unescape_metas : string -> string list val encode_features : (string * real) list -> string val extract_query : string -> string * (string * real) list - val mash_UNLEARN : Proof.context -> unit - val mash_LEARN : - Proof.context -> bool - -> (string * string list * (string * real) list * string list) list -> unit - val mash_RELEARN : - Proof.context -> bool -> (string * string list) list -> unit - val mash_QUERY : - Proof.context -> bool -> int -> string list * (string * real) list - -> (string * real) list + + structure MaSh: + sig + val unlearn : Proof.context -> unit + val learn : + Proof.context -> bool + -> (string * string list * (string * real) list * string list) list -> unit + val relearn : + Proof.context -> bool -> (string * string list) list -> unit + val query : + Proof.context -> bool -> int -> string list * (string * real) list + -> (string * real) list + end + val mash_unlearn : Proof.context -> unit val nickname_of_thm : thm -> string val find_suggested_facts : @@ -215,29 +220,32 @@ map_filter extract_suggestion (space_explode " " suggs)) | _ => ("", []) -fun mash_UNLEARN ctxt = +structure MaSh = +struct + +fun unlearn ctxt = let val path = mash_model_dir () in - trace_msg ctxt (K "MaSh UNLEARN"); + trace_msg ctxt (K "MaSh unlearn"); try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path) NONE; () end -fun mash_LEARN _ _ [] = () - | mash_LEARN ctxt overlord learns = - (trace_msg ctxt (fn () => "MaSh LEARN " ^ +fun learn _ _ [] = () + | learn ctxt overlord learns = + (trace_msg ctxt (fn () => "MaSh learn " ^ elide_string 1000 (space_implode " " (map #1 learns))); run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ())) -fun mash_RELEARN _ _ [] = () - | mash_RELEARN ctxt overlord relearns = - (trace_msg ctxt (fn () => "MaSh RELEARN " ^ +fun relearn _ _ [] = () + | relearn ctxt overlord relearns = + (trace_msg ctxt (fn () => "MaSh relearn " ^ elide_string 1000 (space_implode " " (map #1 relearns))); run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ())) -fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = - (trace_msg ctxt (fn () => "MaSh QUERY " ^ encode_features feats); +fun query ctxt overlord max_suggs (query as (_, feats)) = + (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); run_mash_tool ctxt overlord false max_suggs ([query], str_of_query) (fn suggs => @@ -246,6 +254,8 @@ | suggs => snd (extract_query (List.last suggs))) handle List.Empty => []) +end; + (*** Middle-level communication with MaSh ***) @@ -381,7 +391,7 @@ fun clear_state ctxt = Synchronized.change global_state (fn _ => - (mash_UNLEARN ctxt; (* also removes the state file *) + (MaSh.unlearn ctxt; (* also removes the state file *) (true, empty_state))) end @@ -778,7 +788,7 @@ val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) in - (access_G, mash_QUERY ctxt overlord max_facts (parents, feats)) + (access_G, MaSh.query ctxt overlord max_facts (parents, feats)) end) val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) val unknown = facts |> filter_out (is_fact_in_graph access_G) @@ -834,7 +844,7 @@ in peek_state ctxt (fn {access_G, ...} => let val parents = maximal_in_graph access_G facts in - mash_LEARN ctxt overlord [(name, parents, feats, deps)] + MaSh.learn ctxt overlord [(name, parents, feats, deps)] end); (true, "") end) @@ -892,8 +902,8 @@ (false, SOME names, []) => SOME (map #1 learns @ names) | _ => NONE in - mash_LEARN ctxt overlord (rev learns); - mash_RELEARN ctxt overlord relearns; + MaSh.learn ctxt overlord (rev learns); + MaSh.relearn ctxt overlord relearns; {access_G = access_G, dirty = dirty} end fun commit last learns relearns flops =