# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID cf72aed038c8227483c2bfd186a5a1460f47affd
# Parent  5b9043595b7dcc803aaee8704757802614babb7c
support TFF1 in TPTP parser/interpreter

diff -r 5b9043595b7d -r cf72aed038c8 src/HOL/TPTP/TPTP_Parser/tptp.lex
--- a/src/HOL/TPTP/TPTP_Parser/tptp.lex	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.lex	Thu Aug 07 12:17:41 2014 +0200
@@ -86,6 +86,7 @@
 upper_word                = {upper_alpha}{alpha_numeric}*;
 dollar_dollar_word        = {ddollar}{lower_word};
 dollar_word               = {dollar}{lower_word};
+dollar_underscore         = {dollar}_;
 
 distinct_object           = {double_quote}{do_char}+{double_quote};
 
@@ -177,6 +178,7 @@
 
 {lower_word}   => (col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col));
 {dollar_word}  => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
+{dollar_underscore}  => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
 {dollar_dollar_word}  => (col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col));
 
 "+"           => (col:=yypos-(!eolpos); T.PLUS(!linep,!col));
diff -r 5b9043595b7d -r cf72aed038c8 src/HOL/TPTP/TPTP_Parser/tptp.yacc
--- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Thu Aug 07 12:17:41 2014 +0200
@@ -491,7 +491,7 @@
 tff_unitary_type : tff_atomic_type               (( tff_atomic_type ))
                  | LPAREN tff_xprod_type RPAREN  (( tff_xprod_type ))
 
-tff_atomic_type : atomic_word   (( Atom_type atomic_word ))
+tff_atomic_type : atomic_word   (( Atom_type (atomic_word, []) ))
                 | defined_type  (( Defined_type defined_type ))
                 | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
                 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
@@ -634,6 +634,7 @@
   | "$real" => Type_Real
   | "$rat" => Type_Rat
   | "$int" => Type_Int
+  | "$_" => Type_Dummy
   | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
 ))
 
@@ -747,6 +748,7 @@
   | "$real" => TypeSymbol Type_Real
   | "$rat" => TypeSymbol Type_Rat
   | "$tType" => TypeSymbol Type_Type
+  | "$_" => TypeSymbol Type_Dummy
 
   | "$true" => Interpreted_Logic True
   | "$false" => Interpreted_Logic False
diff -r 5b9043595b7d -r cf72aed038c8 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -8,11 +8,11 @@
 sig
   (*Signature extension: typing information for variables and constants*)
   type var_types = (string * typ option) list
-  type const_map = (string * term) 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 = (TPTP_Syntax.tptp_type * typ) list
+  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
@@ -35,7 +35,7 @@
      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 ->
+  val declare_type : config -> string * (string * int) -> type_map ->
     theory -> type_map * theory
 
   (*Map TPTP types to Isabelle/HOL types*)
@@ -132,9 +132,9 @@
 
 (** Signatures and other type abbrevations **)
 
-type const_map = (string * term) list
+type const_map = (string * (term * int list)) list
 type var_types = (string * typ option) list
-type type_map = (TPTP_Syntax.tptp_type * typ) 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 =
@@ -189,17 +189,19 @@
 (*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 =
+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)
+    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 type} o prefix "'" o string_of_int)
       val thy' =
-        Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy
+        Typedecl.typedecl_global (mk_binding config type_name, tyargs, NoSyn) thy
         |> snd
-      val typ_map_entry = (thf_type, (Type (final_fqn, [])))
+      val typ_map_entry = (thf_type, (final_fqn, arity))
       val ty_map' = typ_map_entry :: ty_map
     in (ty_map', thy') end
 
@@ -217,42 +219,56 @@
     raise MISINTERPRET_TERM
      ("Const already declared", Term_Func (Uninterpreted const_name, []))
   else
-    Theory.specify_const
-     ((mk_binding config const_name, ty), NoSyn) thy
-
-fun declare_const_ifnot config const_name ty thy =
-  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 ty thy
+    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.*)
+(*Types in TFF/THF are encoded as formulas. These functions translate them to type form.*)
+
+fun termtype_to_type (Term_Func (TypeSymbol typ, [])) =
+      Defined_type typ
+  | termtype_to_type (Term_Func (Uninterpreted str, tms)) =
+      Atom_type (str, 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 (Term_Func (TypeSymbol typ, [])))) =
-      Defined_type typ
-  | fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) =
-      Atom_type str
+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
+
+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 type})
 
 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
+    fun lookup_type ty_map ary str =
+      (case AList.lookup (op =) ty_map str of
           NONE =>
-            raise MISINTERPRET_TYPE
+            raise MISINTERPRET_SYMBOL
               ("Could not find the interpretation of this TPTP type in the \
-               \mapping to Isabelle/HOL", thf_ty)
-        | SOME ty => ty)
+               \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) =>
@@ -263,8 +279,10 @@
          Type (@{type_name 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
+     | 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 ind}
@@ -272,7 +290,8 @@
           | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
           | Type_Int => @{typ int}
           | Type_Rat => @{typ rat}
-          | Type_Real => @{typ real})
+          | Type_Real => @{typ real}
+          | Type_Dummy => dummyT)
      | Sum_type _ =>
          raise MISINTERPRET_TYPE (*FIXME*)
           ("No type interpretation (sum type)", thf_ty)
@@ -284,19 +303,15 @@
           ("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, []))
+fun permute_type_args perm Ts = map (nth Ts) perm
+
+fun the_const 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)
+    | _ => raise MISINTERPRET_TERM
+        ("Could not find the interpretation of this constant in the \
+          \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
 
 (*Eta-expands n-ary function.
  "str" is the name of an Isabelle/HOL constant*)
@@ -340,18 +355,24 @@
   | Is_Int => 1
   | Is_Rat => 1
   | Distinct => 1
-  | Apply=> 2
+  | Apply => 2
 
-fun interpret_symbol config language const_map symb thy =
+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))
+    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 language const_map n
+       the_const 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))), [])
+          (string_of_interpreted_symbol interpreted_symbol))), tyargs)
    | Interpreted_Logic logic_symbol =>
        (case logic_symbol of
           Equals => HOLogic.eq_const dummyT
@@ -421,16 +442,14 @@
         in
           case symb of
              Uninterpreted const_name =>
-               declare_const_ifnot config const_name
-                (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I) thy'
-               |> snd
+               perhaps (try (snd o declare_constant config const_name
+                (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I))) thy'
            | _ => thy'
         end
     | Atom_App _ => thy
     | Atom_Arity (const_name, n_args) =>
-        declare_const_ifnot config const_name
-         (mk_fun_type (replicate n_args ind_type) value_type I) thy
-        |> snd
+        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*)
@@ -493,24 +512,32 @@
                (interpret_term formula_level config language const_map
                 var_types type_map (hd tptp_ts)))
            | _ =>
-              (*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_ts) thy')
-                      (interpret_term false config language const_map
-                       var_types type_map (hd tptp_ts))
-                in (interpret_symbol config language const_map symb thy' $ t, thy'')
-                end
-              else
-                (
-                mapply'
-                  (fold_map (interpret_term false config language const_map
-                   var_types type_map) tptp_ts thy')
-                  (`(interpret_symbol config language const_map symb))
-                )
+              let
+                val typ_arity = type_arity_of_symbol thy config symb
+                val (tptp_type_args, tptp_term_args) = chop typ_arity tptp_ts
+                val tyargs =
+                  map (interpret_type config thy type_map o 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
@@ -537,14 +564,12 @@
   | Term_Num (number_kind, num) =>
       let
         (*FIXME hack*)
-        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_"
-      (*FIXME hack -- for Int_num should be
-       HOLogic.mk_number @{typ "int"} (the (Int.fromString num))*)
-      in declare_const_ifnot config (prefix ^ num) ind_type thy end
+        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
   | Term_Distinct_Object str =>
       declare_constant config ("do_" ^ str)
         (interpret_type config thy type_map (Defined_type Type_Ind)) thy
@@ -571,11 +596,9 @@
                  (Atom_Arity (const_name, length tptp_formulas)) thy'
             in
               (if is_prod_typed thy' config symbol then
-                 mtimes thy' args (interpret_symbol config language
-                  const_map symbol thy')
+                 mtimes thy' args (interpret_symbol config const_map symbol [] thy')
                else
-                mapply args
-                 (interpret_symbol config language const_map symbol thy'),
+                mapply args (interpret_symbol config const_map symbol [] thy'),
               thy')
             end
         | _ =>
@@ -587,11 +610,9 @@
                  tptp_formulas thy
             in
               (if is_prod_typed thy' config symbol then
-                 mtimes thy' args (interpret_symbol config language
-                  const_map symbol thy')
+                 mtimes thy' args (interpret_symbol config const_map symbol [] thy')
                else
-                 mapply args
-                  (interpret_symbol config language const_map symbol thy'),
+                 mapply args (interpret_symbol config const_map symbol [] thy'),
                thy')
             end)
     | Sequent _ =>
@@ -663,12 +684,12 @@
         (case tptp_atom of
           TFF_Typed_Atom (symbol, tptp_type_opt) =>
             (*FIXME ignoring type info*)
-            (interpret_symbol config language const_map symbol thy, thy)
+            (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 language const_map symbol thy, thy))
+            (interpret_symbol config const_map symbol [] thy, thy))
     | Type_fmla _ =>
          raise MISINTERPRET_FORMULA
           ("Cannot interpret types as formulas", tptp_fmla)
@@ -678,20 +699,31 @@
 
 (*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 typ => fmlatype_to_type typ
-      | _ => tptp_type
+        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
   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 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)) = (strip_prod_type ty1, ty2)
+  | dest_fn_type ty = ([], ty)
+
 fun resolve_include_path path_prefixes path_suffix =
   case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
          path_prefixes of
@@ -699,6 +731,15 @@
   | NONE =>
     error ("Cannot find include file " ^ quote (Path.implode path_suffix))
 
+(* Ideally, to be in sync with TFF1, 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 (curry (op =) (SOME (Defined_type Type_Type)) o snd) 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) =>
@@ -719,7 +760,7 @@
          case role of
            Role_Type =>
              let
-               val (tptp_ty, name) =
+               val ((tptp_type_vars, 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*))
@@ -727,22 +768,15 @@
                    (typeof_tff_typing tptp_formula,
                     nameof_tff_typing tptp_formula)
              in
-               case tptp_ty of
-                 Defined_type Type_Type => (*add new type*)
+               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
-                         (Atom_type name, name)
-                         type_map
-                         thy
-                    in ((type_map',
-                         const_map,
-                         []),
-                        thy')
-                    end
+                        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
@@ -752,7 +786,7 @@
                     (*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') =
+                    val (t as Const (name', _), thy') =
                       let
                         fun analyse_type thy thf_ty =
                            if #cautious config then
@@ -760,13 +794,13 @@
                                Fn_type (thf_ty1, thf_ty2) =>
                                  (analyse_type thy thf_ty1;
                                  analyse_type thy thf_ty2)
-                             | Atom_type ty_name =>
+                             | 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)
+                                     Atom_type (ty_name, []))
                              | _ => ()
                            else () (*skip test if we're not being cautious.*)
                       in
@@ -778,7 +812,19 @@
                     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)
+
+                    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*)
@@ -792,7 +838,7 @@
                (*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
+                  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.*)
diff -r 5b9043595b7d -r cf72aed038c8 src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -174,9 +174,9 @@
 \\000"
 ),
  (1, 
-"\000\000\000\000\000\000\000\000\000\142\144\000\000\143\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\142\138\133\000\101\089\088\083\082\081\080\078\077\072\070\057\
+"\000\000\000\000\000\000\000\000\000\143\145\000\000\144\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\143\139\134\000\101\089\088\083\082\081\080\078\077\072\070\057\
 \\048\048\048\048\048\048\048\048\048\048\045\000\039\037\036\033\
 \\030\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
 \\029\029\029\029\029\029\029\029\029\029\029\028\000\027\026\000\
@@ -847,10 +847,10 @@
  (101, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\131\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\132\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\131\
 \\000\102\102\128\102\102\124\102\102\118\102\102\108\102\102\102\
 \\102\102\102\102\103\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
@@ -1053,76 +1053,76 @@
 \\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (131, 
-"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
-\\000"
-),
  (132, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\000\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\132\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
 \\000"
 ),
  (133, 
-"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\000\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\137\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134"
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\000\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\133\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
+\\000"
 ),
  (134, 
-"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\136\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\135\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134"
+"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\000\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\138\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135"
 ),
  (135, 
+"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\137\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135"
+),
+ (136, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\134\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\134\000\000\000\
+\\000\000\135\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\135\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
- (138, 
+ (139, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\141\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\140\139\000\
+\\000\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\141\140\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
- (142, 
-"\000\000\000\000\000\000\000\000\000\142\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+ (143, 
+"\000\000\000\000\000\000\000\000\000\143\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\143\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
@@ -1130,8 +1130,8 @@
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
- (143, 
-"\000\000\000\000\000\000\000\000\000\000\144\000\000\000\000\000\
+ (144, 
+"\000\000\000\000\000\000\000\000\000\000\145\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
@@ -1184,7 +1184,7 @@
 {fin = [(N 12)], trans = 0},
 {fin = [(N 78)], trans = 33},
 {fin = [(N 21)], trans = 0},
-{fin = [(N 303)], trans = 0},
+{fin = [(N 306)], trans = 0},
 {fin = [(N 38)], trans = 0},
 {fin = [(N 31)], trans = 37},
 {fin = [(N 48)], trans = 0},
@@ -1193,10 +1193,10 @@
 {fin = [(N 68)], trans = 0},
 {fin = [(N 41)], trans = 42},
 {fin = [(N 45)], trans = 0},
-{fin = [(N 297)], trans = 0},
+{fin = [(N 300)], trans = 0},
 {fin = [(N 27)], trans = 45},
 {fin = [(N 36)], trans = 0},
-{fin = [(N 306)], trans = 0},
+{fin = [(N 309)], trans = 0},
 {fin = [(N 126)], trans = 48},
 {fin = [], trans = 49},
 {fin = [(N 104)], trans = 49},
@@ -1225,11 +1225,11 @@
 {fin = [(N 55)], trans = 0},
 {fin = [(N 123)], trans = 74},
 {fin = [(N 58)], trans = 75},
-{fin = [(N 294)], trans = 0},
+{fin = [(N 297)], trans = 0},
 {fin = [(N 29)], trans = 0},
-{fin = [(N 288)], trans = 78},
+{fin = [(N 291)], trans = 78},
 {fin = [(N 76)], trans = 0},
-{fin = [(N 290)], trans = 0},
+{fin = [(N 293)], trans = 0},
 {fin = [(N 82)], trans = 0},
 {fin = [(N 52)], trans = 0},
 {fin = [], trans = 83},
@@ -1280,19 +1280,20 @@
 {fin = [(N 278)], trans = 128},
 {fin = [(N 278)], trans = 129},
 {fin = [(N 209),(N 278)], trans = 102},
-{fin = [], trans = 131},
-{fin = [(N 286)], trans = 132},
-{fin = [], trans = 133},
+{fin = [(N 281)], trans = 0},
+{fin = [], trans = 132},
+{fin = [(N 289)], trans = 133},
 {fin = [], trans = 134},
 {fin = [], trans = 135},
+{fin = [], trans = 136},
 {fin = [(N 95)], trans = 0},
-{fin = [], trans = 135},
-{fin = [(N 33)], trans = 138},
-{fin = [(N 300)], trans = 0},
+{fin = [], trans = 136},
+{fin = [(N 33)], trans = 139},
+{fin = [(N 303)], trans = 0},
 {fin = [(N 64)], trans = 0},
 {fin = [(N 18)], trans = 0},
-{fin = [(N 2)], trans = 142},
-{fin = [(N 7)], trans = 143},
+{fin = [(N 2)], trans = 143},
+{fin = [(N 7)], trans = 144},
 {fin = [(N 7)], trans = 0}])
 end
 structure StartStates =
@@ -1369,15 +1370,16 @@
 | 27 => (col:=yypos-(!eolpos); T.COLON(!linep,!col))
 | 271 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col) end
 | 278 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
-| 286 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
-| 288 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
+| 281 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
+| 289 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
 | 29 => (col:=yypos-(!eolpos); T.COMMA(!linep,!col))
-| 290 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
-| 294 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
-| 297 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
-| 300 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
-| 303 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
-| 306 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
+| 291 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
+| 293 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
+| 297 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
+| 300 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
+| 303 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
+| 306 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
+| 309 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
 | 31 => (col:=yypos-(!eolpos); T.EQUALS(!linep,!col))
 | 33 => (col:=yypos-(!eolpos); T.EXCLAMATION(!linep,!col))
 | 36 => (col:=yypos-(!eolpos); T.LET(!linep,!col))
@@ -4851,7 +4853,7 @@
 end
 |  ( 135, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left,
  atomic_word1right)) :: rest671)) => let val  result = 
-MlyValue.tff_atomic_type (( Atom_type atomic_word ))
+MlyValue.tff_atomic_type (( Atom_type (atomic_word, []) ))
  in ( LrTable.NT 79, ( result, atomic_word1left, atomic_word1right), 
 rest671)
 end
@@ -5316,6 +5318,7 @@
   | "$real" => Type_Real
   | "$rat" => Type_Rat
   | "$int" => Type_Int
+  | "$_" => Type_Dummy
   | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
 )
 )
@@ -5590,6 +5593,7 @@
   | "$real" => TypeSymbol Type_Real
   | "$rat" => TypeSymbol Type_Rat
   | "$tType" => TypeSymbol Type_Type
+  | "$_" => TypeSymbol Type_Dummy
 
   | "$true" => Interpreted_Logic True
   | "$false" => Interpreted_Logic False
diff -r 5b9043595b7d -r cf72aed038c8 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -66,7 +66,7 @@
     Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
 
   and tptp_base_type =
-    Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
+    Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real | Type_Dummy
 
   and symbol =
       Uninterpreted of string
@@ -111,7 +111,8 @@
   and tptp_type =
       Prod_type of tptp_type * tptp_type
     | Fn_type of tptp_type * tptp_type
-    | Atom_type of string
+    | Atom_type of string * tptp_type list
+    | Var_type of string
     | Defined_type of tptp_base_type
     | Sum_type of tptp_type * tptp_type (*only THF*)
     | Fmla_type of tptp_formula
@@ -141,8 +142,6 @@
 
   val status_to_string : status_value -> string
 
-  val nameof_tff_atom_type : tptp_type -> string
-
   val pos_of_line : tptp_line -> position
 
   (*Returns the list of all files included in a directory and its
@@ -216,7 +215,7 @@
     Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
 
   and tptp_base_type =
-    Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
+    Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real | Type_Dummy
 
   and symbol =
       Uninterpreted of string
@@ -261,7 +260,8 @@
   and tptp_type =
       Prod_type of tptp_type * tptp_type
     | Fn_type of tptp_type * tptp_type
-    | Atom_type of string
+    | Atom_type of string * tptp_type list
+    | Var_type of string
     | Defined_type of tptp_base_type
     | Sum_type of tptp_type * tptp_type
     | Fmla_type of tptp_formula
@@ -287,9 +287,6 @@
 
 fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
 
-fun nameof_tff_atom_type (Atom_type str) = str
-  | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
-
 fun pos_of_line tptp_line =
   case tptp_line of
       Annotated_Formula (position, _, _, _, _, _) => position
@@ -428,6 +425,7 @@
   | string_of_tptp_base_type Type_Int = "$int"
   | string_of_tptp_base_type Type_Rat = "$rat"
   | string_of_tptp_base_type Type_Real = "$real"
+  | string_of_tptp_base_type Type_Dummy = "$_"
 
 and string_of_interpreted_symbol x =
   case x of
@@ -517,7 +515,10 @@
       string_of_tptp_type tptp_type1 ^ " * " ^ string_of_tptp_type tptp_type2
   | string_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) =
       string_of_tptp_type tptp_type1 ^ " > " ^ string_of_tptp_type tptp_type2
-  | string_of_tptp_type (Atom_type str) = str
+  | string_of_tptp_type (Atom_type (str, [])) = str
+  | string_of_tptp_type (Atom_type (str, tptp_types)) =
+      str ^ "(" ^ commas (map string_of_tptp_type tptp_types) ^ ")"
+  | string_of_tptp_type (Var_type str) = str
   | string_of_tptp_type (Defined_type tptp_base_type) =
       string_of_tptp_base_type tptp_base_type
   | string_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = ""
@@ -565,6 +566,7 @@
   | latex_of_tptp_base_type Type_Int = "\\\\mathsf{int} "
   | latex_of_tptp_base_type Type_Rat = "\\\\mathsf{rat} "
   | latex_of_tptp_base_type Type_Real = "\\\\mathsf{real} "
+  | latex_of_tptp_base_type Type_Dummy = "\\\\mathsf{\\\\_} "
 
 and latex_of_interpreted_symbol x =
   case x of
@@ -687,7 +689,10 @@
       latex_of_tptp_type tptp_type1 ^ " \\\\times " ^ latex_of_tptp_type tptp_type2
   | latex_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) =
       latex_of_tptp_type tptp_type1 ^ " \\\\to " ^ latex_of_tptp_type tptp_type2
-  | latex_of_tptp_type (Atom_type str) = "\\\\mathrm{" ^ str ^ "}"
+  | latex_of_tptp_type (Atom_type (str, [])) = "\\\\mathrm{" ^ str ^ "}"
+  | latex_of_tptp_type (Atom_type (str, tptp_types)) =
+    "\\\\mathrm{" ^ str ^ "}(" ^ commas (map latex_of_tptp_type tptp_types) ^ ")"
+  | latex_of_tptp_type (Var_type str) = "\\\\mathrm{" ^ str ^ "}"
   | latex_of_tptp_type (Defined_type tptp_base_type) =
       latex_of_tptp_base_type tptp_base_type
   | latex_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = ""