--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nunchaku/nunchaku_util.ML Fri Sep 08 00:01:36 2017 +0200
@@ -0,0 +1,95 @@
+(* Title: HOL/Nunchaku/Tools/nunchaku_util.ML
+ Author: Jasmin Blanchette, VU Amsterdam
+ Copyright 2015, 2016, 2017
+
+General-purpose functions used by Nunchaku.
+*)
+
+signature NUNCHAKU_UTIL =
+sig
+ val elide_string: int -> string -> string
+ val nat_subscript: int -> string
+ val timestamp: unit -> string
+ val parse_bool_option: bool -> string -> string -> bool option
+ val parse_time: string -> string -> Time.time
+ val string_of_time: Time.time -> string
+ val simplify_spaces: string -> string
+ val ascii_of: string -> string
+ val unascii_of: string -> string
+ val double_lookup: ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
+ val triple_lookup: (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
+ val plural_s_for_list: 'a list -> string
+ val with_overlord_file: string -> string -> (Path.T -> 'a) -> 'a
+ val with_tmp_or_overlord_file: bool -> string -> string -> (Path.T -> 'a) -> 'a
+ val num_binder_types: typ -> int
+ val strip_fun_type: typ -> typ list * typ
+ val attach_typeS: term -> term
+ val specialize_type: theory -> string * typ -> term -> term
+ val typ_match: theory -> typ * typ -> bool
+ val term_match: theory -> term * term -> bool
+ val const_match: theory -> (string * typ) * (string * typ) -> bool
+ val DETERM_TIMEOUT: Time.time -> tactic -> tactic
+ val spying: bool -> (unit -> Proof.state * int * string) -> unit
+end;
+
+structure Nunchaku_Util : NUNCHAKU_UTIL =
+struct
+
+val elide_string = ATP_Util.elide_string;
+val nat_subscript = Nitpick_Util.nat_subscript;
+val timestamp = ATP_Util.timestamp;
+
+val parse_bool_option = Sledgehammer_Util.parse_bool_option;
+val parse_time = Sledgehammer_Util.parse_time;
+val string_of_time = ATP_Util.string_of_time;
+val simplify_spaces = Sledgehammer_Util.simplify_spaces;
+val ascii_of = ATP_Problem_Generate.ascii_of;
+val unascii_of = ATP_Problem_Generate.unascii_of;
+val double_lookup = Nitpick_Util.double_lookup;
+val triple_lookup = Nitpick_Util.triple_lookup;
+val plural_s_for_list = Nitpick_Util.plural_s_for_list;
+
+fun with_overlord_file name ext f =
+ f (Path.explode ("$ISABELLE_HOME_USER/" ^ name ^ "." ^ ext));
+
+fun with_tmp_or_overlord_file overlord =
+ if overlord then with_overlord_file else Isabelle_System.with_tmp_file;
+
+val num_binder_types = BNF_Util.num_binder_types
+val strip_fun_type = BNF_Util.strip_fun_type;
+
+(* Clone from "HOL/Tools/inductive_realizer.ML". *)
+val attach_typeS =
+ map_types (map_atyps
+ (fn TFree (s, []) => TFree (s, @{sort type})
+ | TVar (ixn, []) => TVar (ixn, @{sort type})
+ | T => T));
+
+val specialize_type = ATP_Util.specialize_type;
+
+fun typ_match thy TU = can (Sign.typ_match thy TU) Vartab.empty;
+fun term_match thy tu = can (Pattern.match thy tu) (Vartab.empty, Vartab.empty);
+fun const_match thy = term_match thy o apply2 Const;
+
+val DETERM_TIMEOUT = Nitpick_Util.DETERM_TIMEOUT;
+
+val spying_version = "a"
+
+val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term;
+
+fun spying spy f =
+ if spy then
+ let
+ val (state, i, message) = f ();
+ val ctxt = Proof.context_of state;
+ val goal = Logic.get_goal (Thm.prop_of (#goal (Proof.goal state))) i;
+ val hash =
+ String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12);
+ in
+ File.append (Path.explode "$ISABELLE_HOME_USER/spy_nunchaku")
+ (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n")
+ end
+ else
+ ();
+
+end;