| products/Sources/formale Sprachen/Isabelle/HOL/TPTP/TPTP_Parser/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: tptp_interpret.ML Sprache: SMLOriginal von: Isabelle© |
|
||||||
|
(* Title: HOL/TPTP/TPTP_Parser/tptp_interpret.ML
Author: Nik Sultana, Cambridge University Computer Laboratory Interprets TPTP problems in Isabelle/HOL. *) signature TPTP_INTERPRET = sig (*Signature extension: typing information for variables and constants*) type var_types = (string * typ option) list type const_map = (string * (term * int list)) list (*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 = (string * (string * int)) list (*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 * term * TPTP_Proof.source_info option (*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 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) (*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 = {cautious : 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 -> string * (string * int) -> 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 TPTP terms to Isabelle/HOL terms*) val interpret_term : bool -> config -> TPTP_Syntax.language -> const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> theory -> 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 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, 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: 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_prefixes = paths 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 list -> TPTP_Syntax.tptp_line -> theory -> tptp_general_meaning * theory (*Like "interpret_line" above, but works over a whole parsed problem. Arguments: config = as previously inclusion list = as previously path_prefixes = as previously lines = parsed TPTP syntax type_map = as previously const_map = as previously thy = as previously *) val interpret_problem : config -> string list -> Path.T list -> TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory -> tptp_general_meaning * theory (*Like "interpret_problem" above, but it is given a filename rather than a parsed problem.*) val interpret_file : bool -> Path.T list -> Path.T -> type_map -> const_map -> theory -> tptp_general_meaning * theory type position = string * int * int exception MISINTERPRET of position list * exn 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 val import_file : bool -> Path.T list -> 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 end structure TPTP_Interpret : TPTP_INTERPRET = struct open TPTP_Syntax type position = string * int * int exception MISINTERPRET of position list * exn 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 (* General stuff *) type config = {cautious : bool, problem_name : TPTP_Problem_Name.problem_name option} (* Interpretation *) (** Signatures and other type abbrevations **) type const_map = (string * (term * int list)) list type var_types = (string * typ option) list type type_map = (string * (string * int)) list type tptp_formula_meaning = string * TPTP_Syntax.role * term * TPTP_Proof.source_info option type tptp_general_meaning = (type_map * const_map * tptp_formula_meaning list) type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning structure TPTP_Data = Theory_Data ( type T = manifest list val empty = [] val extend = I fun merge data : T = Library.merge (op =) data ) val get_manifests = TPTP_Data.get (** Adding types to a signature **) (*transform quoted names into acceptable ASCII strings*) fun alphanumerate c = let val c' = ord c val out_of_range = ((c' > 64) andalso (c' < 91)) orelse ((c' > 96) andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58)) in if (not out_of_range) andalso (not (c = "_")) then "_nom_" ^ Int.toString (ord c) ^ "_" else c end fun alphanumerated_name prefix name = prefix ^ (raw_explode #> map alphanumerate #> implode) name fun mk_binding (config : config) ident = let val pre_binding = Binding.name (alphanumerated_name "bnd_" ident) in case #problem_name config of NONE => pre_binding | SOME prob => Binding.qualify false (TPTP_Problem_Name.mangle_problem_name prob) 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, arity)) ty_map thy = if type_exists config thy type_name then raise MISINTERPRET_TYPE ("Type already exists", Atom_type (type_name, [])) else let val binding = mk_binding config type_name val final_fqn = Sign.full_name thy binding val tyargs = List.tabulate (arity, rpair \<^sort>\<open>type\<close> o prefix "'" o string_of_int) val (_, thy') = Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy val typ_map_entry = (thf_type, (final_fqn, arity)) val ty_map' = typ_map_entry :: ty_map in (ty_map', thy') end (** Adding constants to signature **) fun full_name thy config const_name = Sign.full_name thy (mk_binding config const_name) fun const_exists config thy const_name = Sign.declared_const thy (full_name thy config const_name) fun declare_constant config const_name ty thy = if const_exists config thy const_name then raise MISINTERPRET_TERM ("Const already declared", Term_FuncG (Uninterpreted const_name, [], [])) else Theory.specify_const ((mk_binding config const_name, ty), NoSyn) thy (** Interpretation functions **) (*Types in TFF/THF are encoded as formulas. These functions translate them to type form.*) fun termtype_to_type (Term_FuncG (TypeSymbol typ, [], [])) = Defined_type typ | termtype_to_type (Term_FuncG (Uninterpreted str, tys, tms)) = Atom_type (str, tys @ map termtype_to_type tms) | termtype_to_type (Term_Var str) = Var_type str (*FIXME possibly incomplete hack*) fun fmlatype_to_type (Atom (THF_Atom_term tm)) = termtype_to_type tm | fmlatype_to_type (Type_fmla (Fn_type (ty1, ty2))) = let val ty1' = case ty1 of Fn_type _ => fmlatype_to_type (Type_fmla ty1) | Fmla_type ty1 => fmlatype_to_type ty1 | _ => ty1 val ty2' = case ty2 of Fn_type _ => fmlatype_to_type (Type_fmla ty2) | Fmla_type ty2 => fmlatype_to_type ty2 | _ => ty2 in Fn_type (ty1', ty2') end | fmlatype_to_type (Type_fmla ty) = ty | fmlatype_to_type (Fmla (Uninterpreted str, fmla)) = Atom_type (str, map fmlatype_to_type fmla) | fmlatype_to_type (Quant (Dep_Prod, _, fmla)) = fmlatype_to_type fmla | fmlatype_to_type (Pred (Interpreted_ExtraLogic Apply, [tm])) = termtype_to_type tm | fmlatype_to_type (Fmla (Interpreted_ExtraLogic Apply, [tm1, tm2])) = (case fmlatype_to_type tm1 of Atom_type (str, tys) => Atom_type (str, tys @ [fmlatype_to_type tm2])) fun tfree_name_of_var_type str = "'" ^ Name.desymbolize (SOME false) str fun tfree_of_var_type str = TFree (tfree_name_of_var_type str, \<^sort>\<open>type\<close>) fun interpret_type config thy type_map thf_ty = let fun lookup_type ty_map ary str = (case AList.lookup (op =) ty_map str of NONE => raise MISINTERPRET_SYMBOL ("Could not find the interpretation of this TPTP type in the \ \mapping to Isabelle/HOL", Uninterpreted str) | SOME (str', ary') => if ary' = ary then str' else raise MISINTERPRET_SYMBOL ("TPTP type used with wrong arity", Uninterpreted str)) in case thf_ty of Prod_type (thf_ty1, thf_ty2) => Type (\<^type_name>\<open>prod\<close>, [interpret_type config thy type_map thf_ty1, interpret_type config thy type_map thf_ty2]) | Fn_type (thf_ty1, thf_ty2) => Type (\<^type_name>\<open>fun\<close>, [interpret_type config thy type_map thf_ty1, interpret_type config thy type_map thf_ty2]) | Atom_type (str, thf_tys) => Type (lookup_type type_map (length thf_tys) str, map (interpret_type config thy type_map) thf_tys) | Var_type str => tfree_of_var_type str | Defined_type tptp_base_type => (case tptp_base_type of Type_Ind => \<^typ>\<open>ind\<close> | Type_Bool => HOLogic.boolT | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty) (*FIXME these types are currently unsupported, so they're treated as individuals*) (* | Type_Int => @{typ int} | Type_Rat => @{typ rat} | Type_Real => @{typ real} *) | Type_Int => interpret_type config thy type_map (Defined_type Type_Ind) | Type_Rat => interpret_type config thy type_map (Defined_type Type_Ind) | Type_Real => interpret_type config thy type_map (Defined_type Type_Ind) | Type_Dummy => dummyT) | Sum_type _ => raise MISINTERPRET_TYPE (*FIXME*) ("No type interpretation (sum type)", thf_ty) | Fmla_type tptp_ty => fmlatype_to_type tptp_ty |> interpret_type config thy type_map | Subtype _ => raise MISINTERPRET_TYPE (*FIXME*) ("No type interpretation (subtype)", thf_ty) end fun permute_type_args perm Ts = map (nth Ts) perm fun the_const config thy const_map str tyargs = (case AList.lookup (op =) const_map str of SOME (Const (s, _), tyarg_perm) => Sign.mk_const thy (s, permute_type_args tyarg_perm tyargs) | _ => 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_FuncG (Uninterpreted str, [], []))) (*Eta-expands n-ary function. "str" is the name of an Isabelle/HOL constant*) fun mk_n_fun n str = let fun body 0 t = t | body n t = body (n - 1) (t $ (Bound (n - 1))) in body n (Const (str, dummyT)) |> funpow n (Term.absdummy dummyT) end fun mk_fun_type [] b acc = acc b | mk_fun_type (ty :: tys) b acc = mk_fun_type tys b (fn ty_rest => Type ("fun", [ty, acc ty_rest])) (*These arities are not part of the TPTP spec*) fun arity_of interpreted_symbol = case interpreted_symbol of UMinus => 1 | Sum => 2 | Difference => 2 | Product => 2 | Quotient => 2 | Quotient_E => 2 | Quotient_T => 2 | Quotient_F => 2 | Remainder_E => 2 | Remainder_T => 2 | Remainder_F => 2 | Floor => 1 | Ceiling => 1 | Truncate => 1 | Round => 1 | To_Int => 1 | To_Rat => 1 | To_Real => 1 | Less => 2 | LessEq => 2 | Greater => 2 | GreaterEq => 2 | EvalEq => 2 | Is_Int => 1 | Is_Rat => 1 | Distinct => 1 | Apply => 2 fun type_arity_of_symbol thy config (Uninterpreted n) = let val s = full_name thy config n in length (Sign.const_typargs thy (s, Sign.the_const_type thy s)) handle TYPE _ => 0 end | type_arity_of_symbol _ _ _ = 0 fun interpret_symbol config const_map symb tyargs thy = case symb of Uninterpreted n => (*Constant would have been added to the map at the time of declaration*) the_const config thy const_map n tyargs | Interpreted_ExtraLogic interpreted_symbol => (*FIXME not interpreting*) Sign.mk_const thy ((Sign.full_name thy (mk_binding config (string_of_interpreted_symbol interpreted_symbol))), tyargs) | Interpreted_Logic logic_symbol => (case logic_symbol of Equals => HOLogic.eq_const dummyT | NEquals => HOLogic.mk_not (HOLogic.eq_const dummyT $ Bound 1 $ Bound 0) |> (Term.absdummy dummyT #> Term.absdummy dummyT) | Or => HOLogic.disj | And => HOLogic.conj | Iff => HOLogic.eq_const HOLogic.boolT | If => HOLogic.imp | Fi => \<^term>\<open>\<lambda> x. \<lambda> y. y \<longrightarrow> x\<close> | Xor => \<^term>\<open>\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)\<close> | Nor => \<^term>\<open>\<lambda> x. \<lambda> y. \<not> (x \<or> y)\<close> | Nand => \<^term>\<open>\<lambda> x. \<lambda> y. \<not> (x \<and> y)\<close> | Not => HOLogic.Not | Op_Forall => HOLogic.all_const dummyT | Op_Exists => HOLogic.exists_const dummyT | True => \<^term>\<open>True\<close> | False => \<^term>\<open>False\<close> ) | TypeSymbol _ => raise MISINTERPRET_SYMBOL ("Cannot have TypeSymbol in term", symb) | System _ => raise MISINTERPRET_SYMBOL ("Cannot interpret system symbol", symb) (*Apply a function to a list of arguments*) val mapply = fold (fn x => fn y => y $ x) fun mapply' (args, thy) f = let val (f', thy') = f thy in (mapply args f', thy') end (*As above, but for products*) fun mtimes thy = fold (fn x => fn y => Sign.mk_const thy (\<^const_name>\<open>Pair\<close>, [dummyT, dummyT]) $ y $ x) fun mtimes' (args, thy) f = let val (f', thy') = f thy in (mtimes thy' args f', thy') end datatype tptp_atom_value = Atom_App of tptp_term | Atom_Arity of string * int (*FIXME instead of int could use type list*) (*Adds constants to signature when explicit type declaration isn't expected, e.g. FOL. "formula_level" means that the constants are to be interpreted as predicates, otherwise as functions over individuals.*) fun type_atoms_to_thy config formula_level type_map tptp_atom_value thy = let val ind_type = interpret_type config thy type_map (Defined_type Type_Ind) val value_type = if formula_level then interpret_type config thy type_map (Defined_type Type_Bool) else ind_type in case tptp_atom_value of Atom_App (Term_FuncG (symb, tptp_tys, tptp_ts)) => let val thy' = fold (fn t => type_atoms_to_thy config false type_map (Atom_App t)) tptp_ts thy in case symb of Uninterpreted const_name => perhaps (try (snd o declare_constant config const_name (mk_fun_type (replicate (length tptp_tys + length tptp_ts) ind_type) value_type I))) thy' | _ => thy' end | Atom_App _ => thy | Atom_Arity (const_name, n_args) => perhaps (try (snd o declare_constant config const_name (mk_fun_type (replicate n_args ind_type) value_type I))) thy end (*FIXME only used until interpretation is implemented*) fun add_interp_symbols_to_thy config type_map thy = let val ind_symbols = [UMinus, Sum, Difference, Product, Quotient, Quotient_E, Quotient_T, Quotient_F, Remainder_E, Remainder_T, Remainder_F, Floor, Ceiling, Truncate, Round, To_Int, To_Rat, To_Real, Distinct, Apply] val bool_symbols = [Less, LessEq, Greater, GreaterEq, EvalEq, Is_Int, Is_Rat] fun add_interp_symbol_to_thy formula_level symbol = type_atoms_to_thy config formula_level type_map (Atom_Arity (string_of_interpreted_symbol symbol, arity_of symbol)) in fold (add_interp_symbol_to_thy false) ind_symbols thy |> fold (add_interp_symbol_to_thy true) bool_symbols end (*Next batch of functions give info about Isabelle/HOL types*) fun is_fun (Type (\<^type_name>\<open>fun\<close>, _)) = true | is_fun _ = false fun is_prod (Type (\<^type_name>\<open>prod\<close>, _)) = true | is_prod _ = false fun dom_type (Type (\<^type_name>\<open>fun\<close>, [ty1, _])) = ty1 fun is_prod_typed thy config symb = let fun symb_type const_name = Sign.the_const_type thy (full_name thy config const_name) in case symb of Uninterpreted const_name => if is_fun (symb_type const_name) then symb_type const_name |> dom_type |> is_prod else false | _ => false end fun strip_applies_term (Term_FuncG (Interpreted_ExtraLogic Apply, [], [tm1, tm2])) = strip_applies_term tm1 ||> (fn tms => tms @ [tm2]) | strip_applies_term tm = (tm, []) fun termify_apply_fmla thy config (Fmla (Interpreted_ExtraLogic Apply, [fmla1, fmla2])) = (case termify_apply_fmla thy config fmla1 of SOME (Term_FuncG (symb, tys, tms)) => let val typ_arity = type_arity_of_symbol thy config symb in (case (null tms andalso length tys < typ_arity, try fmlatype_to_type fmla2) of (true, SOME ty) => SOME (Term_FuncG (symb, tys @ [ty], [])) | _ => (case termify_apply_fmla thy config fmla2 of SOME tm2 => SOME (Term_FuncG (symb, tys, tms @ [tm2])) | NONE => NONE)) end | _ => NONE) | termify_apply_fmla _ _ (Atom (THF_Atom_term tm)) = SOME tm | termify_apply_fmla _ _ _ = NONE (* Information needed to be carried around: - constant mapping: maps constant names to Isabelle terms with fully-qualified 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' cannot be bound across terms. *) fun interpret_term formula_level config language const_map var_types type_map tptp_t thy = case tptp_t of Term_FuncG (symb, tptp_tys, tptp_ts) => let val thy' = type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy in case symb of Interpreted_ExtraLogic Apply => (case strip_applies_term tptp_t of (Term_FuncG (symb, tptp_tys, tptp_ts), extra_tptp_ts) => interpret_term formula_level config language const_map var_types type_map (Term_FuncG (symb, tptp_tys, tptp_ts @ extra_tptp_ts)) thy | _ => (*apply the head of the argument list to the tail*) (mapply' (fold_map (interpret_term false config language const_map var_types type_map) (tl tptp_ts) thy') (interpret_term formula_level config language const_map var_types type_map (hd tptp_ts)))) | _ => let val typ_arity = type_arity_of_symbol thy' config symb val (tptp_type_args, tptp_term_args) = chop (typ_arity - length tptp_tys) tptp_ts val tyargs = map (interpret_type config thy' type_map) (tptp_tys @ map termtype_to_type tptp_type_args) in (*apply symb to tptp_ts*) if is_prod_typed thy' config symb then let val (t, thy'') = mtimes' (fold_map (interpret_term false config language const_map var_types type_map) (tl tptp_term_args) thy') (interpret_term false config language const_map var_types type_map (hd tptp_term_args)) in (interpret_symbol config const_map symb tyargs thy' $ t, thy'') end else ( mapply' (fold_map (interpret_term false config language const_map var_types type_map) tptp_term_args thy') (`(interpret_symbol config const_map symb tyargs)) ) end end | Term_Var n => (if language = THF orelse language = TFF then (case AList.lookup (op =) var_types n of SOME ty => (case ty of SOME ty => Free (n, ty) | NONE => Free (n, dummyT) (*to infer the variable's type*) ) | NONE => Free (n, dummyT) (*raise MISINTERPRET_TERM ("Could not type variable", tptp_t)*)) else (*variables range over individuals*) Free (n, interpret_type config thy type_map (Defined_type Type_Ind)), thy) | Term_Conditional (tptp_formula, tptp_t1, tptp_t2) => let val (t_fmla, thy') = interpret_formula config language const_map var_types type_map tptp_formula thy val ([t1, t2], thy'') = fold_map (interpret_term formula_level config language const_map var_types type_map) [tptp_t1, tptp_t2] thy' in (mk_n_fun 3 \<^const_name>\<open>If\<close> $ t_fmla $ t1 $ t2, thy'') end | Term_Num (number_kind, num) => let (*FIXME hack*) (* val tptp_type = case number_kind of Int_num => Type_Int | Real_num => Type_Real | Rat_num => Type_Rat val T = interpret_type config thy type_map (Defined_type tptp_type) in (HOLogic.mk_number T (the (Int.fromString num)), thy) end *) val ind_type = interpret_type config thy type_map (Defined_type Type_Ind) val prefix = case number_kind of Int_num => "intn_" | Real_num => "realn_" | Rat_num => "ratn_" val const_name = prefix ^ num in if const_exists config thy const_name then (Sign.mk_const thy ((Sign.full_name thy (mk_binding config const_name)), []), thy) else declare_constant config const_name ind_type thy end | Term_Distinct_Object str => declare_constant config ("do_" ^ str) (interpret_type config thy type_map (Defined_type Type_Ind)) thy and interpret_formula config language const_map var_types type_map tptp_fmla thy = case tptp_fmla of Pred (symb, ts) => interpret_term true config language const_map var_types type_map (Term_FuncG (symb, [], ts)) thy | Fmla (symbol, tptp_formulas) => (case symbol of Interpreted_ExtraLogic Apply => (case termify_apply_fmla thy config tptp_fmla of SOME tptp_t => interpret_term true config language const_map var_types type_map tptp_t thy | NONE => mapply' (fold_map (interpret_formula config language const_map var_types type_map) (tl tptp_formulas) thy) (interpret_formula config language const_map var_types type_map (hd tptp_formulas))) | Uninterpreted const_name => let val (args, thy') = (fold_map (interpret_formula config language const_map var_types type_map) tptp_formulas thy) val thy' = type_atoms_to_thy config true type_map (Atom_Arity (const_name, length tptp_formulas)) thy' in (if is_prod_typed thy' config symbol then mtimes thy' args (interpret_symbol config const_map symbol [] thy') else mapply args (interpret_symbol config const_map symbol [] thy'), thy') end | _ => let val (args, thy') = fold_map (interpret_formula config language const_map var_types type_map) tptp_formulas thy in (if is_prod_typed thy' config symbol then mtimes thy' args (interpret_symbol config const_map symbol [] thy') else mapply args (interpret_symbol config const_map symbol [] thy'), thy') end) | Sequent _ => (*FIXME unsupported*) raise MISINTERPRET_FORMULA ("'Sequent' unsupported", tptp_fmla) | Quant (quantifier, bindings, tptp_formula) => let val var_types' = ListPair.unzip bindings |> (apsnd ((map o Option.map) (interpret_type config thy type_map))) |> ListPair.zip |> List.rev fun fold_bind f = fold (fn (n, ty) => fn t => case ty of NONE => f (n, if language = THF then dummyT else interpret_type config thy type_map (Defined_type Type_Ind), t) | SOME ty => f (n, ty, t) ) var_types' in case quantifier of Forall => interpret_formula config language const_map (var_types' @ var_types) type_map tptp_formula thy |>> fold_bind HOLogic.mk_all | Exists => interpret_formula config language const_map (var_types' @ var_types) type_map tptp_formula thy |>> fold_bind HOLogic.mk_exists | Lambda => interpret_formula config language const_map (var_types' @ var_types) type_map tptp_formula thy |>> fold_bind (fn (n, ty, rest) => lambda (Free (n, ty)) rest) | Epsilon => let val (t, thy') = interpret_formula config language const_map var_types type_map (Quant (Lambda, bindings, tptp_formula)) thy in ((HOLogic.choice_const dummyT) $ t, thy') end | Iota => let val (t, thy') = interpret_formula config language const_map var_types type_map (Quant (Lambda, bindings, tptp_formula)) thy in (Const (\<^const_name>\<open>The\<close>, dummyT) $ t, thy') end | Dep_Prod => raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla) | Dep_Sum => raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla) end | Conditional (fmla1, fmla2, fmla3) => let val interp = interpret_formula config language const_map var_types type_map val (((fmla1', fmla2'), fmla3'), thy') = interp fmla1 thy ||>> interp fmla2 ||>> interp fmla3 in (HOLogic.mk_conj (HOLogic.mk_imp (fmla1', fmla2'), HOLogic.mk_imp (HOLogic.mk_not fmla1', fmla3')), thy') end | Let (tptp_let_list, tptp_formula) => (*FIXME not yet implemented*) raise MISINTERPRET_FORMULA ("'Let' not yet implemented", tptp_fmla) | Atom tptp_atom => (case tptp_atom of TFF_Typed_Atom (symbol, tptp_type_opt) => (*FIXME ignoring type info*) (interpret_symbol config const_map symbol [] thy, thy) | THF_Atom_term tptp_term => interpret_term true config language const_map var_types type_map tptp_term thy | THF_Atom_conn_term symbol => (interpret_symbol config const_map symbol [] thy, thy)) | Type_fmla _ => raise MISINTERPRET_FORMULA ("Cannot interpret types as formulas", tptp_fmla) | THF_typing (tptp_formula, _) => (*FIXME ignoring type info*) interpret_formula config language const_map var_types type_map tptp_formula thy (*Extract the type from a typing*) local fun type_vars_of_fmlatype (Quant (Dep_Prod, varlist, fmla)) = map fst varlist @ type_vars_of_fmlatype fmla | type_vars_of_fmlatype _ = [] fun extract_type tptp_type = case tptp_type of Fmla_type fmla => (type_vars_of_fmlatype fmla, fmlatype_to_type fmla) | _ => ([], tptp_type) in fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type | typeof_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) = extract_type tptp_type end fun nameof_typing (THF_typing ((Atom (THF_Atom_term (Term_FuncG (Uninterpreted str, [], [])))), _)) = str | nameof_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str fun strip_prod_type (Prod_type (ty1, ty2)) = ty1 :: strip_prod_type ty2 | strip_prod_type ty = [ty] fun dest_fn_type (Fn_type (ty1, ty2)) = let val (tys2, ty3) = dest_fn_type ty2 in (strip_prod_type ty1 @ tys2, ty3) end | dest_fn_type ty = ([], ty) fun resolve_include_path path_prefixes path_suffix = case find_first (fn prefix => File.exists (prefix + path_suffix)) path_prefixes of SOME prefix => prefix + path_suffix | NONE => error ("Cannot find include file " ^ Path.print path_suffix) fun is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], [ true | is_type_type (Defined_type Type_Type) = true | is_type_type _ = false; (* Ideally, to be in sync with TFF1/THF1, we should perform full type skolemization here. But the problems originating from HOL systems are restricted to top-level universal quantification for types. *) fun remove_leading_type_quantifiers (Quant (Forall, varlist, tptp_fmla)) = (case filter_out (fn (_, SOME ty) => is_type_type ty | _ => false) varlist of [] => remove_leading_type_quantifiers tptp_fmla | varlist' => Quant (Forall, varlist', tptp_fmla)) | remove_leading_type_quantifiers tptp_fmla = tptp_fmla fun interpret_line config inc_list type_map const_map path_prefixes line thy = case line of Include (_, quoted_path, inc_list) => interpret_file' config inc_list path_prefixes (resolve_include_path path_prefixes (quoted_path |> unenclose |> Path.explode)) type_map const_map thy | Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) => (*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 ((tptp_type_vars, tptp_ty), name) = (typeof_typing tptp_formula (*assuming tptp_formula is a typing*), nameof_typing tptp_formula (*and that the LHS is a (atom) name*)) in case dest_fn_type tptp_ty of (tptp_binders, 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 (name, (name, length tptp_binders)) 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 as Const (name', _), 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 config 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 tf_tyargs = map tfree_of_var_type tptp_type_vars val isa_tyargs = Sign.const_typargs thy' (name', ty) val _ = if length isa_tyargs < length tf_tyargs then raise MISINTERPRET_SYMBOL ("Cannot handle phantom types for constant", Uninterpreted name) else () val tyarg_perm = map (fn T => find_index (curry (op =) T) tf_tyargs) isa_tyargs val const_map' = ((name, (t, tyarg_perm)) :: 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 (remove_leading_type_quantifiers 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, Syntax.check_term (Proof_Context.init_global thy') t, TPTP_Proof.extract_source_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_prefixes lines type_map const_map thy = let val thy_with_symbols = add_interp_symbols_to_thy config type_map thy 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_prefixes line thy (*FIXME handle (*package all exceptions to include position information, even relating to multiple levels of "include"ed files*) (*FIXME "exn" contents may appear garbled due to markup FIXME this appears as ML source position *) MISINTERPRET (pos_list, exn) => raise MISINTERPRET (TPTP_Syntax.pos_of_line line :: pos_list, exn) | exn => raise MISINTERPRET ([TPTP_Syntax.pos_of_line line], exn) *) 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_with_symbols) (*initial values*) end and interpret_file' config inc_list path_prefixes 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 config inc_list path_prefixes else error "Could not determine absolute path to file" end and interpret_file cautious path_prefixes file_name = let val config = {cautious = cautious, problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.file_name file_name)) in interpret_file' config [] path_prefixes file_name end fun import_file cautious path_prefixes file_name type_map const_map thy = let val prob_name = TPTP_Problem_Name.parse_problem_name (Path.file_name file_name) val (result, thy') = interpret_file cautious path_prefixes file_name type_map const_map thy (*FIXME doesn't check if problem has already been interpreted*) in TPTP_Data.map (cons ((prob_name, result))) thy' end val _ = Outer_Syntax.command \<^command_keyword>\<open>import_tptp\<close> "import TPTP problem" (Parse.path >> (fn name => Toplevel.theory (fn thy => let val path = Path.explode name (*NOTE: assumes include files are located at $TPTP/Axioms (which is how TPTP is organised)*) in import_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy end))) end ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
