(* 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
(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
type var_types = (string * typ option) 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.*)
type type_map = (TPTP_Syntax.tptp_type * typ) list
(*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*)
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.*)
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*)
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*)}
(*map types form TPTP to Isabelle/HOL*)
val interpret_type : config -> theory -> type_map ->
TPTP_Syntax.tptp_type -> typ
(*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.
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.
Arguments:
cautious = indicates whether additional checks are made to check
that all used types have been declared.
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.
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 ->
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 = " "
*)
val interpret_problem : bool -> config -> 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
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
(*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
val extract_inference_info : (TPTP_Syntax.general_term * 'a list) option ->
(string * string list) option
end
structure TPTP_Interpret : TPTP_INTERPRET =
struct
open TPTP_Syntax
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 =
{(*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*)}
(* Interpretation *)
(** Signatures and other type abbrevations **)
type const_map = (string * term) list
type var_types = (string * typ option) list
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
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
(*SMLNJ complains if non-expanded form used below*)
fun merge v = Library.merge (op =) v)
val get_manifests = TPTP_Data.get
(** Adding types to a signature **)
fun type_exists thy ty_name =
Sign.declared_tyname thy (Sign.full_bname thy ty_name)
val IND_TYPE = "ind"
(*SMLNJ complains if type annotation not used below*)
fun mk_binding (config : config) ident =
let
val pre_binding = Binding.name 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
(*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
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 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
(** 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_Func (Uninterpreted const_name, []))
else
Theory.specify_const
((mk_binding config const_name, ty), NoSyn) thy
(** Interpretation **)
(*Types in THF are encoded as formulas. This function translates them to type form.*)
(*FIXME possibly incomplete hack*)
fun fmlatype_to_type (Atom (THF_Atom_term (Term_Func (TypeSymbol typ, [])))) =
Defined_type typ
| fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) =
Atom_type str
| 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
val ty2' = case ty2 of
Fn_type _ => fmlatype_to_type (Type_fmla ty2)
| Fmla_type ty2 => fmlatype_to_type ty2
in Fn_type (ty1', ty2') end
fun interpret_type config thy type_map thf_ty =
let
fun lookup_type ty_map thf_ty =
(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)
| SOME ty => ty)
in
case thf_ty of (*FIXME make tail*)
Prod_type (thf_ty1, thf_ty2) =>
Type ("Product_Type.prod",
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
| Fn_type (thf_ty1, thf_ty2) =>
Type ("fun",
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
| Atom_type _ =>
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_Bool => HOLogic.boolT
| 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*)
| Type_Rat =>
interpret_type config thy type_map (Defined_type Type_Ind)
| Type_Real =>
interpret_type config thy type_map (Defined_type Type_Ind)
)
| 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 the_const config thy language const_map_payload str =
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, []))
| 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, []))
(*Eta-expands Isabelle/HOL binary function.
"str" is the name of a polymorphic constant in Isabelle/HOL*)
fun mk_fun str =
(Const (str, Term.dummyT) $ Bound 1 $ Bound 0)
|> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
(*As above, but swaps the function's arguments*)
fun mk_swapped_fun str =
(Const (str, Term.dummyT) $ Bound 0 $ Bound 1)
|> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
fun dummy_term () =
HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"}
fun interpret_symbol config thy language const_map symb =
case symb of
Uninterpreted n =>
(*Constant would have been added to the map at the time of
declaration*)
the_const config thy language const_map n
| Interpreted_ExtraLogic interpreted_symbol =>
(case interpreted_symbol of (*FIXME incomplete,
and doesn't work with $i*)
Sum => mk_fun @{const_name Groups.plus}
| UMinus =>
(Const (@{const_name Groups.uminus}, Term.dummyT) $ Bound 0)
|> Term.absdummy Term.dummyT
| Difference => mk_fun @{const_name Groups.minus}
| Product => mk_fun @{const_name Groups.times}
| Quotient => mk_fun @{const_name Fields.divide}
| Less => mk_fun @{const_name Orderings.less}
| LessEq => mk_fun @{const_name Orderings.less_eq}
| Greater => mk_swapped_fun @{const_name Orderings.less}
(*FIXME would be nicer to expand "greater"
and "greater_eq" abbreviations*)
| GreaterEq => mk_swapped_fun @{const_name Orderings.less_eq}
(* FIXME todo
| Quotient_E | Quotient_T | Quotient_F | Remainder_E | Remainder_T
| Remainder_F | Floor | Ceiling | Truncate | Round | To_Int | To_Rat
| To_Real | EvalEq | Is_Int | Is_Rat*)
| Apply => raise MISINTERPRET_SYMBOL ("Malformed term?", symb)
| _ => dummy_term ()
)
| Interpreted_Logic logic_symbol =>
(case logic_symbol of
Equals => HOLogic.eq_const Term.dummyT
| NEquals =>
HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0)
|> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
| Or => HOLogic.disj
| And => HOLogic.conj
| Iff => HOLogic.eq_const HOLogic.boolT
| If => HOLogic.imp
| Fi => @{term "\<lambda> x. \<lambda> y. y \<longrightarrow> x"}
| Xor =>
@{term
"\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)"}
| Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}
| Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}
| Not => HOLogic.Not
| Op_Forall => HOLogic.all_const Term.dummyT
| Op_Exists => HOLogic.exists_const Term.dummyT
| True => @{term "True"}
| False => @{term "False"}
)
| TypeSymbol _ =>
raise MISINTERPRET_SYMBOL
("Cannot have TypeSymbol in term", symb)
| System str =>
raise MISINTERPRET_SYMBOL
("How to interpret system terms?", symb)
(*Apply a function to a list of arguments*)
val mapply = fold (fn x => fn y => y $ x)
(*As above, but for products*)
fun mtimes thy =
fold (fn x => fn y =>
Sign.mk_const thy
("Product_Type.Pair",[Term.dummyT, Term.dummyT]) $ y $ x)
(*Adds constants to signature in FOL. "formula_level" means that the constants
are to be interpreted as predicates, otherwise as functions over individuals.*)
fun FO_const_types config formula_level type_map tptp_t 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_t of
Term_Func (symb, tptp_ts) =>
let
val thy' = fold (FO_const_types config false type_map) tptp_ts thy
val ty = fold (fn ty1 => fn ty2 => Type ("fun", [ty1, ty2]))
(map (fn _ => ind_type) tptp_ts) value_type
in
case symb of
Uninterpreted const_name =>
if const_exists config thy' const_name then thy'
else snd (declare_constant config const_name ty thy')
| _ => thy'
end
| _ => thy
end
(*like FO_const_types but works over symbols*)
fun symb_const_types config type_map formula_level const_name n_args 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 interpret_type config thy type_map (Defined_type Type_Ind)
fun mk_i_fun b n acc =
if n = 0 then acc b
else
mk_i_fun b (n - 1) (fn ty => Type ("fun", [ind_type, acc ty]))
in
if const_exists config thy const_name then thy
else
snd (declare_constant config const_name
(mk_i_fun value_type n_args I) thy)
end
(*Next batch of functions give info about Isabelle/HOL types*)
fun is_fun (Type ("fun", _)) = true
| is_fun _ = false
fun is_prod (Type ("Product_Type.prod", _)) = true
| is_prod _ = false
fun dom_type (Type ("fun", [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
(*
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' can't be bound across
terms.
*)
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
val thy' = FO_const_types config formula_level type_map tptp_t thy
fun typeof_const const_name = Sign.the_const_type thy'
(Sign.full_name thy' (mk_binding config const_name))
in
case symb of
Interpreted_ExtraLogic Apply =>
(*apply the head of the argument list to the tail*)
(mapply
(map (interpret_term false config language thy' const_map
var_types type_map #> fst) (tl tptp_ts))
(interpret_term formula_level config language thy' const_map
var_types type_map (hd tptp_ts) |> fst),
thy')
| _ =>
(*apply symb to tptp_ts*)
if is_prod_typed thy' config symb then
(interpret_symbol config thy' language const_map symb $
mtimes thy'
(map (interpret_term false config language thy' const_map
var_types type_map #> fst) (tl tptp_ts))
((interpret_term false config language thy' const_map
var_types type_map #> fst) (hd tptp_ts)),
thy')
else
(mapply
(map (interpret_term false config language thy' const_map
var_types type_map #> fst) tptp_ts)
(interpret_symbol config thy' language const_map symb),
thy')
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, Term.dummyT) (*to infer the variable's type*)
)
| NONE =>
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) =>
(mk_fun @{const_name If}, thy)
| Term_Num (number_kind, num) =>
let
val num_term =
if number_kind = Int_num then
HOLogic.mk_number @{typ "int"} (the (Int.fromString num))
else dummy_term () (*FIXME: not yet supporting rationals and reals*)
in (num_term, thy) end
| Term_Distinct_Object str =>
let
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
val mangle_name = raw_explode #> map alphanumerate #> implode
in declare_constant config (mangle_name str)
(interpret_type config thy type_map (Defined_type Type_Ind)) thy
end
(*Given a list of "'a option", then applies a function to each element if that
element is SOME value, otherwise it leaves it as NONE.*)
fun map_opt f xs =
fold
(fn x => fn y =>
(if Option.isSome x then
SOME (f (Option.valOf x))
else NONE) :: y
) xs []
fun interpret_formula config language const_map var_types type_map tptp_fmla thy =
case tptp_fmla of
Pred app =>
interpret_term true config language thy const_map
var_types type_map (Term_Func app)
| Fmla (symbol, tptp_formulas) =>
(case symbol of
Interpreted_ExtraLogic Apply =>
let
val (args, thy') = (fold_map (interpret_formula config language
const_map var_types type_map) (tl tptp_formulas) thy)
val (func, thy') = interpret_formula config language const_map
var_types type_map (hd tptp_formulas) thy'
in (mapply args func, thy') end
| Uninterpreted const_name =>
let
val (args, thy') = (fold_map (interpret_formula config language
const_map var_types type_map) tptp_formulas thy)
val thy' = symb_const_types config type_map true const_name
(length tptp_formulas) thy'
in
(if is_prod_typed thy' config symbol then
mtimes thy' args (interpret_symbol config thy' language
const_map symbol)
else
mapply args
(interpret_symbol config thy' language const_map symbol),
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 thy' language
const_map symbol)
else
mapply args
(interpret_symbol config thy' language const_map symbol),
thy')
end)
| Sequent _ =>
raise MISINTERPRET_FORMULA ("Sequent", tptp_fmla) (*FIXME unsupported*)
| 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)
(interpret_type config thy type_map) bound_var_types
val var_types' =
ListPair.zip (bound_vars, List.rev bound_var_types')
|> List.rev
fun fold_bind f =
fold
(fn (n, ty) => fn t =>
case ty of
NONE =>
f (n,
if language = THF then Term.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 Term.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 The}, Term.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 thy language const_map symbol, thy)
| THF_Atom_term tptp_term =>
interpret_term true config language thy const_map var_types
type_map tptp_term
| THF_Atom_conn_term symbol =>
(interpret_symbol config thy language const_map symbol, thy))
| Type_fmla _ => (*FIXME unsupported*)
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 name of inference rule, and the inferences it relies on*)
(*This is tuned to work with LEO-II, and is brittle to upstream
changes of the proof protocol.*)
fun extract_inference_info annot =
let
fun get_line_id (General_Data (Number (Int_num, num))) = [num]
| get_line_id (General_Data (Atomic_Word name)) = [name]
| get_line_id (General_Term (Number (Int_num, num), _ (*e.g. a bind*))) = [num]
| get_line_id _ = []
(*e.g. General_Data (Application ("theory", [General_Data
(Atomic_Word "equality")])) -- which would come from E through LEO-II*)
in
case annot of
NONE => NONE
| SOME annot =>
(case annot of
(General_Data (Application ("inference",
[General_Data (Atomic_Word inference_name),
_,
General_List related_lines])), _) =>
(SOME (inference_name, map get_line_id related_lines |> List.concat))
| _ => NONE)
end
(*Extract the type from a typing*)
local
fun extract_type tptp_type =
case tptp_type of
Fmla_type typ => fmlatype_to_type typ
| _ => tptp_type
in
fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type
fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) =
extract_type tptp_type
end
fun nameof_typing
(THF_typing
((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 =
case line of
Include (quoted_path, _) => (*FIXME currently everything is imported*)
interpret_file'
false
config
path_prefix
(Path.append
path_prefix
(quoted_path
|> unenclose
|> Path.explode))
type_map
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') =
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
("This 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,
extract_inference_info annotation_opt)]), thy')
end
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_file' new_basic_types config 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
else error "Could not determine absolute path to file."
end
and interpret_file cautious path_prefix file_name =
let
val config =
{cautious = cautious,
problem_name =
SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
file_name))
}
handle _(*FIXME*) =>
{cautious = cautious,
problem_name = NONE
}
in interpret_file' true config path_prefix file_name end
fun import_file cautious path_prefix file_name type_map const_map thy =
let
val prob_name =
TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
handle _(*FIXME*) => TPTP_Problem_Name.Nonstandard (Path.implode file_name)
val (result, thy') =
interpret_file cautious path_prefix file_name type_map const_map thy
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
(Parse.path >> (fn path =>
Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
(*Used for debugging. Returns all files contained within a directory or its
subdirectories. Follows symbolic links, filters away directories.*)
fun get_file_list path =
let
fun check_file_entry f rest =
let
(*NOTE needed since don't have File.is_link and File.read_link*)
val f_str = Path.implode f
in
if File.is_dir f then
rest (*filter out directories*)
else if OS.FileSys.isLink f_str then
(*follow links -- NOTE this breaks if links are relative paths*)
check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest
else f :: rest
end
in
File.read_dir path
|> map
(Path.explode
#> Path.append path)
|> (fn l => fold check_file_entry l [])
end
end