# HG changeset patch # User sultana # Date 1334675647 -3600 # Node ID 6062bc362a95d0d6c3bc74632f4c000adc0d2ab1 # Parent 6f215c2ebd727bb841e0be9bc65749a370932f04 tuned diff -r 6f215c2ebd72 -r 6062bc362a95 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 17 16:14:06 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 17 16:14:07 2012 +0100 @@ -211,7 +211,9 @@ let val binding = mk_binding config type_name val final_fqn = Sign.full_name thy binding - val thy' = Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy |> snd + val thy' = + Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy + |> snd val typ_map_entry = (thf_type, (Type (final_fqn, []))) val ty_map' = typ_map_entry :: ty_map in (ty_map', thy') end @@ -258,8 +260,8 @@ (case AList.lookup (op =) ty_map thf_ty of NONE => raise MISINTERPRET_TYPE - ("Could not find the interpretation of this TPTP type in the " ^ - "mapping to Isabelle/HOL", thf_ty) + ("Could not find the interpretation of this TPTP type in the \ + \mapping to Isabelle/HOL", thf_ty) | SOME ty => ty) in case thf_ty of (*FIXME make tail*) @@ -275,12 +277,9 @@ lookup_type type_map thf_ty | Defined_type tptp_base_type => (case tptp_base_type of - Type_Ind => - lookup_type type_map thf_ty + Type_Ind => lookup_type type_map thf_ty | Type_Bool => HOLogic.boolT - | Type_Type => - raise MISINTERPRET_TYPE - ("No type interpretation", thf_ty) + | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty) | Type_Int => Type ("Int.int", []) (*FIXME these types are currently unsupported, so they're treated as individuals*) @@ -304,15 +303,15 @@ if language = THF then (case AList.lookup (op =) const_map_payload str of NONE => raise MISINTERPRET_TERM - ("Could not find the interpretation of this constant in the " ^ - "mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])) + ("Could not find the interpretation of this constant in the \ + \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])) | SOME t => t) else if const_exists config thy str then Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), []) else raise MISINTERPRET_TERM - ("Could not find the interpretation of this constant in the " ^ - "mapping to Isabelle/HOL: ", Term_Func (Uninterpreted str, [])) + ("Could not find the interpretation of this constant in the \ + \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])) (*Eta-expands Isabelle/HOL binary function. "str" is the name of a polymorphic constant in Isabelle/HOL*) @@ -383,7 +382,7 @@ ("Cannot have TypeSymbol in term", symb) | System str => raise MISINTERPRET_SYMBOL - ("How to interpret system terms?", symb) + ("Cannot interpret system symbol", symb) (*Apply a function to a list of arguments*) val mapply = fold (fn x => fn y => y $ x) @@ -466,7 +465,8 @@ after each call of interpret_term since variables' can't be bound across terms. *) -fun interpret_term formula_level config language thy const_map var_types type_map tptp_t = +fun interpret_term formula_level config language thy const_map var_types type_map + tptp_t = case tptp_t of Term_Func (symb, tptp_ts) => let @@ -596,12 +596,14 @@ thy') end) | Sequent _ => - raise MISINTERPRET_FORMULA ("Sequent", tptp_fmla) (*FIXME unsupported*) + (*FIXME unsupported*) + raise MISINTERPRET_FORMULA ("'Sequent' unsupported", tptp_fmla) | Quant (quantifier, bindings, tptp_formula) => let val (bound_vars, bound_var_types) = ListPair.unzip bindings val bound_var_types' : typ option list = - (map_opt : (tptp_type -> typ) -> (tptp_type option list) -> typ option list) + (map_opt : (tptp_type -> typ) -> + (tptp_type option list) -> typ option list) (interpret_type config thy type_map) bound_var_types val var_types' = ListPair.zip (bound_vars, List.rev bound_var_types') @@ -671,7 +673,7 @@ type_map tptp_term | THF_Atom_conn_term symbol => (interpret_symbol config thy language const_map symbol, thy)) - | Type_fmla _ => (*FIXME unsupported*) + | Type_fmla _ => raise MISINTERPRET_FORMULA ("Cannot interpret types as formulas", tptp_fmla) | THF_typing (tptp_formula, _) => (*FIXME ignoring type info*) @@ -759,8 +761,8 @@ if type_exists thy ty_name then () else raise MISINTERPRET_TYPE - ("This type, in signature of " ^ - name ^ " has not been declared.", + ("Type (in signature of " ^ + name ^ ") has not been declared", Atom_type ty_name) | _ => () else () (*skip test if we're not being cautious.*) @@ -838,7 +840,7 @@ Path.implode file_name |> TPTP_Parser.parse_file |> interpret_problem new_basic_types config path_prefix - else error "Could not determine absolute path to file." + else error "Could not determine absolute path to file" end and interpret_file cautious path_prefix file_name =