# HG changeset patch # User sultana # Date 1334675647 -3600 # Node ID 016ce79deb01b22e24aba208cd7debd925c70301 # Parent 6062bc362a95d0d6c3bc74632f4c000adc0d2ab1 enforced 'include' restrictions diff -r 6062bc362a95 -r 016ce79deb01 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 17 16:14:07 2012 +0100 @@ -57,6 +57,15 @@ val interpret_type : config -> theory -> type_map -> TPTP_Syntax.tptp_type -> typ + (*map terms form TPTP to Isabelle/HOL*) + val interpret_term : bool -> config -> TPTP_Syntax.language -> theory -> + const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> + term * theory + + val interpret_formula : config -> TPTP_Syntax.language -> const_map -> + var_types -> type_map -> TPTP_Syntax.tptp_formula -> theory -> + term * theory + (*interpret a TPTP line: return an updated theory including the types & constants which were specified in that formula, a map from constant names to their types, and a map from constant names to Isabelle/HOL @@ -77,16 +86,7 @@ thy = theory where interpreted info will be stored. *) - (*map terms form TPTP to Isabelle/HOL*) - val interpret_term : bool -> config -> TPTP_Syntax.language -> theory -> - const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> - term * theory - - val interpret_formula : config -> TPTP_Syntax.language -> const_map -> - var_types -> type_map -> TPTP_Syntax.tptp_formula -> theory -> - term * theory - - val interpret_line : config -> type_map -> const_map -> + val interpret_line : config -> string list -> type_map -> const_map -> Path.T -> TPTP_Syntax.tptp_line -> theory -> tptp_general_meaning * theory (*Like "interpret_line" above, but works over a whole parsed problem. @@ -103,7 +103,7 @@ const_map = " " thy = " " *) - val interpret_problem : bool -> config -> Path.T -> + val interpret_problem : bool -> config -> string list -> Path.T -> TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory -> tptp_general_meaning * theory @@ -696,12 +696,13 @@ ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str -fun interpret_line config type_map const_map path_prefix line thy = +fun interpret_line config inc_list type_map const_map path_prefix line thy = case line of - Include (quoted_path, _) => (*FIXME currently everything is imported*) + Include (quoted_path, inc_list) => interpret_file' false config + inc_list path_prefix (Path.append path_prefix @@ -712,134 +713,141 @@ const_map thy | Annotated_Formula (pos, lang, label, role, tptp_formula, annotation_opt) => - case role of - Role_Type => - let - val thy_name = Context.theory_name thy - val (tptp_ty, name) = - if lang = THF then - (typeof_typing tptp_formula (*assuming tptp_formula is a typing*), - nameof_typing tptp_formula (*and that the LHS is a (atom) name*)) - else - (typeof_tff_typing tptp_formula, - nameof_tff_typing tptp_formula) - in - case tptp_ty of - Defined_type Type_Type => (*add new type*) - (*generate an Isabelle/HOL type to interpret this TPTP type, - and add it to both the Isabelle/HOL theory and to the type_map*) - let - val (type_map', thy') = - declare_type - config - (Atom_type name, name) - type_map - thy - in ((type_map', - const_map, - []), - thy') - end - - | _ => (*declaration of constant*) - (*Here we populate the map from constants to the Isabelle/HOL - terms they map to (which in turn contain their types).*) - let - val ty = interpret_type config thy type_map tptp_ty - (*make sure that the theory contains all the types appearing - in this constant's signature. Exception is thrown if encounter - an undeclared types.*) - val (t, thy') = + (*interpret a line only if "label" is in "inc_list", or if "inc_list" is + empty (in which case interpret all lines)*) + (*FIXME could work better if inc_list were sorted*) + if null inc_list orelse is_some (List.find (fn x => x = label) inc_list) then + case role of + Role_Type => + let + val thy_name = Context.theory_name thy + val (tptp_ty, name) = + if lang = THF then + (typeof_typing tptp_formula (*assuming tptp_formula is a typing*), + nameof_typing tptp_formula (*and that the LHS is a (atom) name*)) + else + (typeof_tff_typing tptp_formula, + nameof_tff_typing tptp_formula) + in + case tptp_ty of + Defined_type Type_Type => (*add new type*) + (*generate an Isabelle/HOL type to interpret this TPTP type, + and add it to both the Isabelle/HOL theory and to the type_map*) let - fun analyse_type thy thf_ty = - if #cautious config then - case thf_ty of - Fn_type (thf_ty1, thf_ty2) => - (analyse_type thy thf_ty1; - analyse_type thy thf_ty2) - | Atom_type ty_name => - if type_exists thy ty_name then () - else - raise MISINTERPRET_TYPE - ("Type (in signature of " ^ - name ^ ") has not been declared", - Atom_type ty_name) - | _ => () - else () (*skip test if we're not being cautious.*) - in - analyse_type thy tptp_ty; - declare_constant config name ty thy + val (type_map', thy') = + declare_type + config + (Atom_type name, name) + type_map + thy + in ((type_map', + const_map, + []), + thy') end - (*register a mapping from name to t. Constants' type - declarations should occur at most once, so it's justified to - use "::". Note that here we use a constant's name rather - than the possibly- new one, since all references in the - theory will be to this name.*) - val const_map' = ((name, t) :: const_map) - in ((type_map,(*type_map unchanged, since a constant's - declaration shouldn't include any new types.*) - const_map',(*typing table of constant was extended*) - []),(*no formulas were interpreted*) - thy')(*theory was extended with new constant*) - end - end - - | _ => (*i.e. the AF is not a type declaration*) - let - (*gather interpreted term, and the map of types occurring in that term*) - val (t, thy') = - interpret_formula config lang - const_map [] type_map tptp_formula thy - |>> HOLogic.mk_Trueprop - (*type_maps grow monotonically, so return the newest value (type_mapped); - there's no need to unify it with the type_map parameter.*) - in - ((type_map, const_map, - [(label, role, tptp_formula, - Syntax.check_term (Proof_Context.init_global thy') t, - TPTP_Proof.extract_inference_info annotation_opt)]), thy') - end + + | _ => (*declaration of constant*) + (*Here we populate the map from constants to the Isabelle/HOL + terms they map to (which in turn contain their types).*) + let + val ty = interpret_type config thy type_map tptp_ty + (*make sure that the theory contains all the types appearing + in this constant's signature. Exception is thrown if encounter + an undeclared types.*) + val (t, thy') = + let + fun analyse_type thy thf_ty = + if #cautious config then + case thf_ty of + Fn_type (thf_ty1, thf_ty2) => + (analyse_type thy thf_ty1; + analyse_type thy thf_ty2) + | Atom_type ty_name => + if type_exists thy ty_name then () + else + raise MISINTERPRET_TYPE + ("Type (in signature of " ^ + name ^ ") has not been declared", + Atom_type ty_name) + | _ => () + else () (*skip test if we're not being cautious.*) + in + analyse_type thy tptp_ty; + declare_constant config name ty thy + end + (*register a mapping from name to t. Constants' type + declarations should occur at most once, so it's justified to + use "::". Note that here we use a constant's name rather + than the possibly- new one, since all references in the + theory will be to this name.*) + val const_map' = ((name, t) :: const_map) + in ((type_map,(*type_map unchanged, since a constant's + declaration shouldn't include any new types.*) + const_map',(*typing table of constant was extended*) + []),(*no formulas were interpreted*) + thy')(*theory was extended with new constant*) + end + end + + | _ => (*i.e. the AF is not a type declaration*) + let + (*gather interpreted term, and the map of types occurring in that term*) + val (t, thy') = + interpret_formula config lang + const_map [] type_map tptp_formula thy + |>> HOLogic.mk_Trueprop + (*type_maps grow monotonically, so return the newest value (type_mapped); + there's no need to unify it with the type_map parameter.*) + in + ((type_map, const_map, + [(label, role, tptp_formula, + 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 new_basic_types config path_prefix lines type_map const_map thy = - let - val thy_name = Context.theory_name thy - (*Add interpretation of $o and generate an Isabelle/HOL type to - interpret $i, unless we've been given a mapping of types.*) - val (thy', type_map') = - if not new_basic_types then (thy, type_map) - else - let - val (type_map', thy') = - declare_type config - (Defined_type Type_Ind, IND_TYPE) type_map thy - in - (thy', type_map') - end - in - fold (fn line => - fn ((type_map, const_map, lines), thy) => - let - (*process the line, ignoring the type-context for variables*) - val ((type_map', const_map', l'), thy') = - interpret_line config type_map const_map path_prefix line thy - in - ((type_map', - const_map', - l' @ lines),(*append is sufficient, union would be overkill*) - thy') - end) - lines (*lines of the problem file*) - ((type_map', const_map, []), thy') (*initial values*) - end +and interpret_problem new_basic_types config inc_list path_prefix lines + type_map const_map thy = + let + val thy_name = Context.theory_name thy + (*Add interpretation of $o and generate an Isabelle/HOL type to + interpret $i, unless we've been given a mapping of types.*) + val (thy', type_map') = + if not new_basic_types then (thy, type_map) + else + let + val (type_map', thy') = + declare_type config + (Defined_type Type_Ind, IND_TYPE) type_map thy + in + (thy', type_map') + end + in + fold (fn line => + fn ((type_map, const_map, lines), thy) => + let + (*process the line, ignoring the type-context for variables*) + val ((type_map', const_map', l'), thy') = + interpret_line config inc_list type_map const_map path_prefix line thy + in + ((type_map', + const_map', + l' @ lines),(*append is sufficient, union would be overkill*) + thy') + end) + lines (*lines of the problem file*) + ((type_map', const_map, []), thy') (*initial values*) + end -and interpret_file' new_basic_types config path_prefix file_name = +and interpret_file' new_basic_types config inc_list path_prefix file_name = let val file_name' = Path.expand file_name in if Path.is_absolute file_name' then Path.implode file_name |> TPTP_Parser.parse_file - |> interpret_problem new_basic_types config path_prefix + |> interpret_problem new_basic_types config inc_list path_prefix else error "Could not determine absolute path to file" end @@ -855,7 +863,7 @@ {cautious = cautious, problem_name = NONE } - in interpret_file' true config path_prefix file_name end + in interpret_file' true config [] path_prefix file_name end fun import_file cautious path_prefix file_name type_map const_map thy = let