(*  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 = []
  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