1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 17:33:11 2012 +0100
1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 17:33:11 2012 +0100
1.3 @@ -27,10 +27,7 @@
1.4
1.5 text "... and display nicely."
1.6 ML {*
1.7 - List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
1.8 -
1.9 - (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
1.10 - List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
1.11 + List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
1.12 *}
1.13
1.14 subsection "Multiple tests"
2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 17:33:11 2012 +0100
2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 17:33:11 2012 +0100
2.3 @@ -22,7 +22,7 @@
2.4 the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and
2.5 inference info*)
2.6 type tptp_formula_meaning =
2.7 - string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
2.8 + string * TPTP_Syntax.role * term * inference_info
2.9
2.10 (*In general, the meaning of a TPTP statement (which, through the Include
2.11 directive, may include the meaning of an entire TPTP file, is a map from
2.12 @@ -36,15 +36,7 @@
2.13 problem_name = if given then it is used to qualify types & constants*)
2.14 type config =
2.15 {cautious : bool,
2.16 - problem_name : TPTP_Problem_Name.problem_name option
2.17 - (*FIXME future extensibility
2.18 - init_type_map : type_map with_origin,
2.19 - init_const_map : type_map with_origin,
2.20 - dont_build_maps : bool,
2.21 - extend_given_type_map : bool,
2.22 - extend_given_const_map : bool,
2.23 - generative_type_interpretation : bool,
2.24 - generative_const_interpretation : bool*)}
2.25 + problem_name : TPTP_Problem_Name.problem_name option}
2.26
2.27 (*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
2.28 val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
2.29 @@ -149,7 +141,7 @@
2.30 type type_map = (TPTP_Syntax.tptp_type * typ) list
2.31 type inference_info = (string * string list) option
2.32 type tptp_formula_meaning =
2.33 - string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
2.34 + string * TPTP_Syntax.role * term * inference_info
2.35 type tptp_general_meaning =
2.36 (type_map * const_map * tptp_formula_meaning list)
2.37
2.38 @@ -165,9 +157,6 @@
2.39
2.40 (** Adding types to a signature **)
2.41
2.42 -fun type_exists thy ty_name =
2.43 - Sign.declared_tyname thy (Sign.full_bname thy ty_name)
2.44 -
2.45 (*transform quoted names into acceptable ASCII strings*)
2.46 fun alphanumerate c =
2.47 let
2.48 @@ -197,11 +186,14 @@
2.49 pre_binding
2.50 end
2.51
2.52 +fun type_exists config thy ty_name =
2.53 + Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name))
2.54 +
2.55 (*Returns updated theory and the name of the final type's name -- i.e. if the
2.56 original name is already taken then the function looks for an available
2.57 alternative. It also returns an updated type_map if one has been passed to it.*)
2.58 fun declare_type (config : config) (thf_type, type_name) ty_map thy =
2.59 - if type_exists thy type_name then
2.60 + if type_exists config thy type_name then
2.61 raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)
2.62 else
2.63 let
2.64 @@ -260,7 +252,7 @@
2.65 \mapping to Isabelle/HOL", thf_ty)
2.66 | SOME ty => ty)
2.67 in
2.68 - case thf_ty of (*FIXME make tail*)
2.69 + case thf_ty of
2.70 Prod_type (thf_ty1, thf_ty2) =>
2.71 Type ("Product_Type.prod",
2.72 [interpret_type config thy type_map thf_ty1,
2.73 @@ -744,7 +736,7 @@
2.74 (analyse_type thy thf_ty1;
2.75 analyse_type thy thf_ty2)
2.76 | Atom_type ty_name =>
2.77 - if type_exists thy ty_name then ()
2.78 + if type_exists config thy ty_name then ()
2.79 else
2.80 raise MISINTERPRET_TYPE
2.81 ("Type (in signature of " ^
2.82 @@ -781,13 +773,12 @@
2.83 there's no need to unify it with the type_map parameter.*)
2.84 in
2.85 ((type_map, const_map,
2.86 - [(label, role, tptp_formula,
2.87 + [(label, role,
2.88 Syntax.check_term (Proof_Context.init_global thy') t,
2.89 TPTP_Proof.extract_inference_info annotation_opt)]), thy')
2.90 end
2.91 else (*do nothing if we're not to includ this AF*)
2.92 ((type_map, const_map, []), thy)
2.93 -
2.94 and interpret_problem config inc_list path_prefix lines type_map const_map thy =
2.95 let
2.96 val thy_name = Context.theory_name thy
3.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 17:33:11 2012 +0100
3.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 17:33:11 2012 +0100
3.3 @@ -9,8 +9,7 @@
3.4 uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
3.5 begin
3.6
3.7 -import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p" (*FIXME multiple imports*)
3.8 -(*import_tptp "$TPTP_PROBLEMS_PATH/NUM/NUM021^1.p"*)
3.9 +import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
3.10
3.11 ML {*
3.12 val an_fmlas =
3.13 @@ -22,7 +21,7 @@
3.14
3.15 (*Display nicely.*)
3.16 ML {*
3.17 -List.app (fn (n, role, _, fmla, _) =>
3.18 +List.app (fn (n, role, fmla, _) =>
3.19 Pretty.writeln
3.20 (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
3.21 TPTP_Syntax.role_to_string role ^ "): "), Syntax.pretty_term @{context} fmla])
3.22 @@ -35,9 +34,9 @@
3.23 fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
3.24 (string * term) list =
3.25 let
3.26 - fun role_predicate (_, role, _, _, _) =
3.27 + fun role_predicate (_, role, _, _) =
3.28 fold (fn r1 => fn b => role = r1 orelse b) roles false
3.29 - in filter role_predicate #> map (fn (n, _, _, t, _) => (n, t)) end
3.30 + in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
3.31 *}
3.32
3.33 ML {*