# HG changeset patch
# User blanchet
# Date 1401291753 -7200
# Node ID 52e1e424eec18d63d216522642cb526c5edbe114
# Parent  bf5ddf4ec64b29ab07a15a88bb03a823cf800185
export more ML functions, for experimentation

diff -r bf5ddf4ec64b -r 52e1e424eec1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 16:16:40 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 17:42:33 2014 +0200
@@ -34,6 +34,27 @@
   val encode_features : (string * real) list -> string
   val extract_suggestions : string -> string * string list
 
+  datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
+
+  structure MaSh_Py :
+  sig
+    val unlearn : Proof.context -> bool -> unit
+    val learn : Proof.context -> bool -> bool ->
+      (string * string list * string list * string list) list -> unit
+    val relearn : Proof.context -> bool -> bool -> (string * string list) list -> unit
+    val query : Proof.context -> bool -> int ->
+      (string * string list * string list * string list) list * string list * string list
+        * (string * real) list ->
+      string list
+  end
+
+  structure MaSh_SML :
+  sig
+    val query : Proof.context -> mash_engine -> string list -> int ->
+      (string * (string * real) list * string list) list * string list * (string * real) list ->
+      string list
+  end
+
   val mash_unlearn : Proof.context -> params -> unit
   val nickname_of_thm : thm -> string
   val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
@@ -507,7 +528,7 @@
 
 fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
 
-fun query ctxt engine visible_facts max_suggs (learns, hints, parents, feats) =
+fun query ctxt engine visible_facts max_suggs (learns, hints, feats) =
   let
     val visible_fact_set = Symtab.make_set visible_facts
 
@@ -1278,7 +1299,7 @@
           val learns =
             Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
         in
-          MaSh_SML.query ctxt engine visible_facts max_facts (learns, hints, parents, feats)
+          MaSh_SML.query ctxt engine visible_facts max_facts (learns, hints, feats)
         end
 
     val unknown = filter_out (is_fact_in_graph access_G o snd) facts