1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -55,21 +55,27 @@
     1.4  open Sledgehammer_Filter_Iter
     1.5  open Sledgehammer_Provers
     1.6  
     1.7 +val mash_dir = "mash"
     1.8 +val model_file = "model"
     1.9 +val state_file = "state"
    1.10 +
    1.11 +fun mash_path file = getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file
    1.12 +
    1.13  
    1.14  (*** Low-level communication with MaSh ***)
    1.15  
    1.16  fun mash_RESET () =
    1.17 -  tracing "MaSh RESET"
    1.18 +  warning "MaSh RESET"
    1.19  
    1.20 -fun mash_ADD fact (access, feats, deps) =
    1.21 -  tracing ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
    1.22 +fun mash_ADD fact access feats deps =
    1.23 +  warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
    1.24             space_implode " " feats ^ "; " ^ space_implode " " deps)
    1.25  
    1.26  fun mash_DEL fact =
    1.27 -  tracing ("MaSh DEL " ^ fact)
    1.28 +  warning ("MaSh DEL " ^ fact)
    1.29  
    1.30 -fun mash_SUGGEST fact (access, feats) =
    1.31 -  tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
    1.32 +fun mash_SUGGEST access feats =
    1.33 +  warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^
    1.34             space_implode " " feats)
    1.35  
    1.36  
    1.37 @@ -371,18 +377,82 @@
    1.38  
    1.39  (*** High-level communication with MaSh ***)
    1.40  
    1.41 -fun mash_reset () = ()
    1.42 +type mash_state =
    1.43 +  {completed_thys : unit Symtab.table,
    1.44 +   thy_facts : string list Symtab.table}
    1.45  
    1.46 -fun mash_can_suggest_facts () = true
    1.47 +val mash_zero =
    1.48 +  {completed_thys = Symtab.empty,
    1.49 +   thy_facts = Symtab.empty}
    1.50 +
    1.51 +local
    1.52 +
    1.53 +fun mash_load (state as (true, _)) = state
    1.54 +  | mash_load _ =
    1.55 +    (true,
    1.56 +     case mash_path state_file |> Path.explode |> File.read_lines of
    1.57 +       [] => mash_zero
    1.58 +     | comp_line :: facts_lines =>
    1.59 +       let
    1.60 +         fun comp_thys_of_line comp_line =
    1.61 +           Symtab.make (comp_line |> space_explode " " |> map (rpair ()))
    1.62 +         fun add_facts_line line =
    1.63 +           case space_explode " " line of
    1.64 +             thy :: facts => Symtab.update_new (thy, facts)
    1.65 +           | _ => I (* shouldn't happen *)
    1.66 +       in
    1.67 +         {completed_thys = comp_thys_of_line comp_line,
    1.68 +          thy_facts = fold add_facts_line facts_lines Symtab.empty}
    1.69 +       end)
    1.70 +
    1.71 +fun mash_save ({completed_thys, thy_facts} : mash_state) =
    1.72 +  let
    1.73 +    val path = mash_path state_file |> Path.explode
    1.74 +    val comp_line = (completed_thys |> Symtab.keys |> space_implode " ") ^ "\n"
    1.75 +    fun fact_line_for (thy, facts) = space_implode " " (thy :: facts) ^ "\n"
    1.76 +  in
    1.77 +    File.write path comp_line;
    1.78 +    Symtab.fold (fn thy_fact => fn () =>
    1.79 +                    File.append path (fact_line_for thy_fact)) thy_facts
    1.80 +  end
    1.81 +
    1.82 +val state =
    1.83 +  Synchronized.var "Sledgehammer_Filter_MaSh.state" (false, mash_zero)
    1.84 +
    1.85 +in
    1.86 +
    1.87 +fun mash_change f =
    1.88 +  Synchronized.change state (apsnd (tap mash_save o f) o mash_load)
    1.89 +
    1.90 +fun mash_value () = Synchronized.change_result state (`snd o mash_load)
    1.91 +
    1.92 +end
    1.93 +
    1.94 +fun mash_reset () = mash_change (fn _ => (mash_RESET (); mash_zero))
    1.95 +
    1.96 +fun mash_can_suggest_facts () =
    1.97 +  not (Symtab.is_empty (#thy_facts (mash_value ())))
    1.98  
    1.99  fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts =
   1.100 -  (facts, [])
   1.101 +  let
   1.102 +    val access = []
   1.103 +    val feats = []
   1.104 +    val suggs = mash_SUGGEST access feats
   1.105 +  in (facts, []) end
   1.106  
   1.107 -fun mash_can_learn_thy thy = true
   1.108 +fun mash_can_learn_thy thy =
   1.109 +  not (Symtab.defined (#completed_thys (mash_value ()))
   1.110 +                      (Context.theory_name thy))
   1.111  
   1.112  fun mash_learn_thy thy timeout = ()
   1.113  
   1.114  fun mash_learn_proof thy t ths = ()
   1.115 +(*###
   1.116 +  let
   1.117 +  in
   1.118 +    mash_ADD
   1.119 +  end
   1.120 +*)
   1.121  
   1.122  fun relevant_facts ctxt params prover max_facts
   1.123          ({add, only, ...} : fact_override) hyp_ts concl_t facts =