src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML

exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;

(*  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) 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 = (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 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 * 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 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 -> (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 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

  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_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:
      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 : 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 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

  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 -> 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
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) 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 * 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 **)

(*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

(*SMLNJ complains if type annotation not used below*)
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) 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 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 functions **)

(*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
       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 => @{typ ind}
          | 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
        ("Cannot interpret system symbol", 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