# HG changeset patch
# User sultana
# Date 1333553356 -3600
# Node ID 5a1ff6bcf3dc76aad66932e03cfc0d0cb26c3c04
# Parent  26c4e431ef0554bae9711193e40980a2d561c52a
added interpretation for formula conditional;

diff -r 26c4e431ef05 -r 5a1ff6bcf3dc src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 04 16:29:16 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 04 16:29:16 2012 +0100
@@ -651,14 +651,19 @@
         | Dep_Sum =>
             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
         end
-  (*FIXME unsupported
-    | Conditional of tptp_formula * tptp_formula * tptp_formula
-    | Let of tptp_let list * tptp_formula
-
-    and tptp_let =
-        Let_fmla of (string * tptp_type option) * tptp_formula (*both TFF and THF*)
-      | Let_term of (string * tptp_type option) * tptp_term  (*only TFF*)
-  *)
+    | 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) =>