--- a/src/HOL/Nunchaku/Tools/nunchaku_util.ML Thu Sep 07 23:13:15 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_util.ML
- Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII
- Copyright 2015, 2016
-
-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;