# HG changeset patch
# User sultana
# Date 1335180203 -3600
# Node ID 4c681ad99818aee967d7a8b5be44d50566525785
# Parent  f5c05e51668ff439c86096d274d1b918e5c1c278
disabled interpreting arithmetic;

diff -r f5c05e51668f -r 4c681ad99818 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 23 12:23:23 2012 +0100
@@ -269,9 +269,10 @@
             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_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 =>
@@ -322,28 +323,8 @@
        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 ()
-        )
+       (*FIXME make constant, if not interpreting*)
+       dummy_term ()
    | Interpreted_Logic logic_symbol =>
        (case logic_symbol of
           Equals => HOLogic.eq_const Term.dummyT
@@ -522,9 +503,13 @@
   | Term_Num (number_kind, num) =>
       let
         val num_term =
+          (*FIXME
           if number_kind = Int_num then
             HOLogic.mk_number @{typ "int"} (the (Int.fromString num))
           else dummy_term () (*FIXME: not yet supporting rationals and reals*)
+           *)
+          (*FIXME make constant*)
+          dummy_term ()
       in (num_term, thy) end
   | Term_Distinct_Object str =>
       declare_constant config ("do_" ^ str)