# HG changeset patch # User sultana # Date 1334766791 -3600 # Node ID 60849d8c457d204a9b2810995bdc46d06ff435ad # Parent 1a5dc8377b5c40c2defbdc9b75b06e8d796baf4c fixed type interpretation; output now excludes parsed term; tuned; diff -r 1a5dc8377b5c -r 60849d8c457d src/HOL/TPTP/TPTP_Interpret_Test.thy --- 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" diff -r 1a5dc8377b5c -r 60849d8c457d src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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 diff -r 1a5dc8377b5c -r 60849d8c457d src/HOL/TPTP/TPTP_Parser_Example.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 {*