# HG changeset patch # User sultana # Date 1334675647 -3600 # Node ID e84838b78b6d2905d1cc908452ac767c43e1e7d7 # Parent 0a870584145fee8b58cfa1f2025875e080c6792c tuned comments diff -r 0a870584145f -r e84838b78b6d 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 @@ -6,58 +6,55 @@ signature TPTP_INTERPRET = sig - (*signature extension: typing information for variables and constants - (note that the former isn't really part of the signature, but it's bundled - along for more configurability -- though it's probably useless and could be - dropped in the future.*) - type const_map = (string * term) list + (*Signature extension: typing information for variables and constants*) type var_types = (string * typ option) list + type const_map = (string * term) list - (*mapping from TPTP types to Isabelle/HOL types. This map works over all - base types (i.e. TPTP functions must be interpreted as Isabelle/HOL functions). - The map must be total wrt TPTP types. Later on there could be a configuration - option to make a map extensible.*) + (*Mapping from TPTP types to Isabelle/HOL types. This map works over all + base types. The map must be total wrt TPTP types.*) type type_map = (TPTP_Syntax.tptp_type * typ) list - (*inference info, when available, consists of the name of the inference rule + (*Inference info, when available, consists of the name of the inference rule and the names of the inferences involved in the reasoning step.*) type inference_info = (string * string list) option - (*a parsed annotated formula is represented as a triple consisting of - the formula's label, its role, and a constant function to its Isabelle/HOL - term meaning*) + (*A parsed annotated formula is represented as a 5-tuple consisting of + 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 (*In general, the meaning of a TPTP statement (which, through the Include - directive, may include the meaning of an entire TPTP file, is an extended - Isabelle/HOL theory, an explicit map from constants to their Isabelle/HOL - counterparts and their types, the meaning of any TPTP formulas encountered - while interpreting that statement, and a map from TPTP to Isabelle/HOL types - (these types would have been added to the theory returned in the first position - of the tuple). The last value is NONE when the function which produced the - whole tptp_general_meaning value was given a type_map argument -- since - this means that the type_map is already known, and it has not been changed.*) + directive, may include the meaning of an entire TPTP file, is a map from + TPTP to Isabelle/HOL types, a map from TPTP constants to their Isabelle/HOL + counterparts and their types, and a list of interpreted annotated formulas.*) type tptp_general_meaning = (type_map * const_map * tptp_formula_meaning list) - (*if problem_name is given then it is used to qualify types & constants*) + (*cautious = indicates whether additional checks are made to check + that all used types have been declared. + problem_name = if given then it is used to qualify types & constants*) type config = - {(*init_type_map : type_map with_origin, - init_const_map : type_map with_origin,*) - cautious : bool, + {cautious : bool, problem_name : TPTP_Problem_Name.problem_name option - (*dont_build_maps : bool, + (*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*)} - (*map types form TPTP to Isabelle/HOL*) + (*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 -> + theory -> type_map * theory + + (*Map TPTP types to Isabelle/HOL types*) val interpret_type : config -> theory -> type_map -> TPTP_Syntax.tptp_type -> typ - (*map terms form TPTP to Isabelle/HOL*) + (*Map TPTP terms to Isabelle/HOL terms*) val interpret_term : bool -> config -> TPTP_Syntax.language -> theory -> const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> term * theory @@ -66,73 +63,69 @@ 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 - constants; and a list possible formulas resulting from that line. + (*Interpret a TPTP line: return a "tptp_general_meaning" for that line, + as well as an updated Isabelle theory including any types & constants + which were specified in that line. Note that type/constant declarations do not result in any formulas being - returned. A typical TPTP line might update the theory, or return a single - formula. The sole exception is the "include" directive which may update the - theory and also return a list of formulas from the included file. + returned. A typical TPTP line might update the theory, and/or return one or + more formulas. For instance, the "include" directive may update the theory + and also return a list of formulas from the included file. Arguments: - cautious = indicates whether additional checks are made to check - that all used types have been declared. + config = (see above) + inclusion list = names of annotated formulas to interpret (since "include" + directive can be selective wrt to such names) type_map = mapping of TPTP-types to Isabelle/HOL types. This argument may be given to force a specific mapping: this is usually done for using an imported TPTP problem in Isar. const_map = as previous, but for constants. path_prefix = path where TPTP problems etc are located (to help the "include" directive find the files. + line = parsed TPTP line thy = theory where interpreted info will be stored. *) - 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. Arguments: new_basic_types = indicates whether interpretations of $i and $o - types are to be added to the type map (unless it is Given). - This is "true" if we are running this over a fresh TPTP problem, but - "false" if we are calling this _during_ the interpretation of a TPTP file - (i.e. when interpreting an "include" directive. - config = config - path_prefix = " " - contents = parsed TPTP syntax - type_map = see "interpret_line" - const_map = " " - thy = " " + types are to be added to the type map. This is "true" if we are + running this over a fresh TPTP problem, but "false" if we are + calling this _during_ the interpretation of a TPTP file + (i.e. when interpreting an "include" directive). + config = as previously + inclusion list = as previously + path_prefix = as previously + lines = parsed TPTP syntax + type_map = as previously + const_map = as previously + thy = as previously *) val interpret_problem : bool -> config -> string list -> Path.T -> TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory -> tptp_general_meaning * theory - (*Like "interpret_problem" above, but it's given a filename rather than + (*Like "interpret_problem" above, but it is given a filename rather than a parsed problem.*) val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map -> theory -> tptp_general_meaning * theory - (*General exception for this signature.*) exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type - (*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 -> - theory -> type_map * theory + val import_file : bool -> Path.T -> Path.T -> type_map -> const_map -> + theory -> theory + + (*Imported TPTP files are stored as "manifests" in the theory.*) + type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning + val get_manifests : theory -> manifest list (*Returns the list of all files included in a directory and its subdirectories. This is only used for testing the parser/interpreter against all TPTP problems.*) val get_file_list : Path.T -> Path.T list - - type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning - - val get_manifests : theory -> manifest list - - val import_file : bool -> Path.T -> Path.T -> type_map -> const_map -> - theory -> theory end structure TPTP_Interpret : TPTP_INTERPRET = @@ -144,18 +137,13 @@ exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type + (* General stuff *) type config = - {(*init_type_map : type_map with_origin, - init_const_map : type_map with_origin,*) - cautious : bool, - problem_name : TPTP_Problem_Name.problem_name option - (*dont_build_maps : bool, - extend_given_type_map : bool, - extend_given_const_map : bool, - generative_type_interpretation : bool, - generative_const_interpretation : bool*)} + {cautious : bool, + problem_name : TPTP_Problem_Name.problem_name option} + (* Interpretation *) @@ -251,7 +239,7 @@ ((mk_binding config const_name, ty), NoSyn) thy -(** Interpretation **) +(** Interpretation functions **) (*Types in THF are encoded as formulas. This function translates them to type form.*) (*FIXME possibly incomplete hack*) @@ -477,7 +465,7 @@ names. This is fixed, and it is determined by declaration lines earlier in the script (i.e. constants must be declared before appearing in terms. - type context: maps bound variables to their Isabelle type. This is discarded - after each call of interpret_term since variables' can't be bound across + after each call of interpret_term since variables' cannot be bound across terms. *) fun interpret_term formula_level config language thy const_map var_types type_map