# HG changeset patch
# User blanchet
# Date 1434984963 -7200
# Node ID a62655f925c85fd31c14d36aa9043c8c14e2c296
# Parent  dcb0b9b42fcb1ee816bbf26d68ad8627bbb9d5b5
reverted some too aggressive TPTP interpreter changes

diff -r dcb0b9b42fcb -r a62655f925c8 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Jun 22 16:56:03 2015 +0200
@@ -288,9 +288,19 @@
             Type_Ind => @{typ ind}
           | 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*)
@@ -305,13 +315,17 @@
 
 fun permute_type_args perm Ts = map (nth Ts) perm
 
-fun the_const thy const_map str tyargs =
+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)
-    | _ => raise MISINTERPRET_TERM
-        ("Could not find the interpretation of this constant in the \
-          \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
+    | _ =>
+      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 n-ary function.
  "str" is the name of an Isabelle/HOL constant*)
@@ -360,6 +374,7 @@
 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
 
@@ -368,7 +383,7 @@
      Uninterpreted n =>
        (*Constant would have been added to the map at the time of
        declaration*)
-       the_const thy const_map n tyargs
+       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
@@ -513,10 +528,10 @@
                 var_types type_map (hd tptp_ts)))
            | _ =>
               let
-                val typ_arity = type_arity_of_symbol thy config symb
+                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)
+                  map (interpret_type config thy' type_map o termtype_to_type)
                     tptp_type_args
               in
                 (*apply symb to tptp_ts*)
@@ -564,12 +579,27 @@
   | 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