--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 17:33:11 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 17:33:11 2012 +0100
@@ -27,10 +27,7 @@
text "... and display nicely."
ML {*
- List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
-
- (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
- List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
+ List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
*}
subsection "Multiple tests"
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 17:33:11 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 17:33:11 2012 +0100
@@ -22,7 +22,7 @@
the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and
inference info*)
type tptp_formula_meaning =
- string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
+ string * TPTP_Syntax.role * term * inference_info
(*In general, the meaning of a TPTP statement (which, through the Include
directive, may include the meaning of an entire TPTP file, is a map from
@@ -36,15 +36,7 @@
problem_name = if given then it is used to qualify types & constants*)
type config =
{cautious : bool,
- problem_name : TPTP_Problem_Name.problem_name option
- (*FIXME future extensibility
- init_type_map : type_map with_origin,
- init_const_map : type_map with_origin,
- dont_build_maps : bool,
- extend_given_type_map : bool,
- extend_given_const_map : bool,
- generative_type_interpretation : bool,
- generative_const_interpretation : bool*)}
+ problem_name : TPTP_Problem_Name.problem_name option}
(*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
@@ -149,7 +141,7 @@
type type_map = (TPTP_Syntax.tptp_type * typ) list
type inference_info = (string * string list) option
type tptp_formula_meaning =
- string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
+ string * TPTP_Syntax.role * term * inference_info
type tptp_general_meaning =
(type_map * const_map * tptp_formula_meaning list)
@@ -165,9 +157,6 @@
(** Adding types to a signature **)
-fun type_exists thy ty_name =
- Sign.declared_tyname thy (Sign.full_bname thy ty_name)
-
(*transform quoted names into acceptable ASCII strings*)
fun alphanumerate c =
let
@@ -197,11 +186,14 @@
pre_binding
end
+fun type_exists config thy ty_name =
+ Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name))
+
(*Returns updated theory and the name of the final type's name -- i.e. if the
original name is already taken then the function looks for an available
alternative. It also returns an updated type_map if one has been passed to it.*)
fun declare_type (config : config) (thf_type, type_name) ty_map thy =
- if type_exists thy type_name then
+ if type_exists config thy type_name then
raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)
else
let
@@ -260,7 +252,7 @@
\mapping to Isabelle/HOL", thf_ty)
| SOME ty => ty)
in
- case thf_ty of (*FIXME make tail*)
+ case thf_ty of
Prod_type (thf_ty1, thf_ty2) =>
Type ("Product_Type.prod",
[interpret_type config thy type_map thf_ty1,
@@ -744,7 +736,7 @@
(analyse_type thy thf_ty1;
analyse_type thy thf_ty2)
| Atom_type ty_name =>
- if type_exists thy ty_name then ()
+ if type_exists config thy ty_name then ()
else
raise MISINTERPRET_TYPE
("Type (in signature of " ^
@@ -781,13 +773,12 @@
there's no need to unify it with the type_map parameter.*)
in
((type_map, const_map,
- [(label, role, tptp_formula,
+ [(label, role,
Syntax.check_term (Proof_Context.init_global thy') t,
TPTP_Proof.extract_inference_info annotation_opt)]), thy')
end
else (*do nothing if we're not to includ this AF*)
((type_map, const_map, []), thy)
-
and interpret_problem config inc_list path_prefix lines type_map const_map thy =
let
val thy_name = Context.theory_name thy
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 17:33:11 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 17:33:11 2012 +0100
@@ -9,8 +9,7 @@
uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
begin
-import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p" (*FIXME multiple imports*)
-(*import_tptp "$TPTP_PROBLEMS_PATH/NUM/NUM021^1.p"*)
+import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
ML {*
val an_fmlas =
@@ -22,7 +21,7 @@
(*Display nicely.*)
ML {*
-List.app (fn (n, role, _, fmla, _) =>
+List.app (fn (n, role, fmla, _) =>
Pretty.writeln
(Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
TPTP_Syntax.role_to_string role ^ "): "), Syntax.pretty_term @{context} fmla])
@@ -35,9 +34,9 @@
fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
(string * term) list =
let
- fun role_predicate (_, role, _, _, _) =
+ fun role_predicate (_, role, _, _) =
fold (fn r1 => fn b => role = r1 orelse b) roles false
- in filter role_predicate #> map (fn (n, _, _, t, _) => (n, t)) end
+ in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
*}
ML {*