--- a/src/HOL/TPTP/TPTP_Interpret.thy Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret.thy Thu Aug 07 12:17:41 2014 +0200
@@ -14,4 +14,64 @@
ML_file "TPTP_Parser/tptp_interpret.ML"
+
+ML {*
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Systems
+
+fun exploded_absolute_path file_name =
+ Path.explode file_name
+ |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD"))
+
+fun read_tptp_file thy postproc file_name =
+ let
+ fun has_role role (_, role', _, _) = (role' = role)
+ fun get_prop f (name, _, P, _) =
+ let val P' = P |> f |> close_form in
+ (name, P') |> postproc
+ end
+ val path = exploded_absolute_path file_name
+ val ((_, _, problem), thy) =
+ TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"]
+ path [] [] thy
+ val (conjs, defs_and_nondefs) =
+ problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
+ ||> List.partition (has_role TPTP_Syntax.Role_Definition)
+ in
+ (map (get_prop I) conjs,
+ pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
+ Proof_Context.init_global thy)
+ end
+*}
+
+declare [[ML_exception_trace]]
+
+setup {*
+snd o Theory.specify_const ((@{binding c}, @{typ "'b * 'a"}), NoSyn)
+*}
+
+ML {* Sign.the_const_type @{theory} @{const_name c} *}
+
+declare [[ML_print_depth = 1000]]
+
+ML {*
+let
+ val (conjs, (defs, nondefs), _) = read_tptp_file @{theory} snd (* "/Users/blanchet/tmp/e.tptp" *)
+ "/Users/blanchet/.isabelle/prob_alt_ergo_1"
+ val ts = conjs @ defs @ nondefs
+ |> map (map_aterms (fn Const (s, T) =>
+ if String.isPrefix "TPTP" s then
+ Const (s |> Long_Name.base_name |> perhaps (try (unprefix "bnd_")), T)
+ else
+ Const (s, T)
+ | t => t))
+in
+ tracing (cat_lines (map (Syntax.string_of_term_global @{theory}) ts));
+ tracing (cat_lines (map @{make_string} ts))
+end
+*}
+
end
\ No newline at end of file