# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID b870759ce0f3972700b11973a84110a908fbc2c4
# Parent  4dce7f2bb59fb5d541068db404ae1d6727a79fb5
added new metis mode, with no implementation yet

diff -r 4dce7f2bb59f -r b870759ce0f3 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -11,7 +11,7 @@
 sig
   type type_literal = ATP_Translate.type_literal
 
-  datatype mode = FO | HO | FT
+  datatype mode = FO | HO | FT | New
 
   type metis_problem =
     {axioms: (Metis_Thm.thm * thm) list,
@@ -113,11 +113,13 @@
 (* HOL to FOL  (Isabelle to Metis)                                           *)
 (* ------------------------------------------------------------------------- *)
 
-datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
+(* first-order, higher-order, fully-typed, new *)
+datatype mode = FO | HO | FT | New
 
 fun string_of_mode FO = "FO"
   | string_of_mode HO = "HO"
   | string_of_mode FT = "FT"
+  | string_of_mode New = "New"
 
 fun fn_isa_to_met_sublevel "equal" = "c_fequal"
   | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
@@ -293,15 +295,18 @@
   end;
 
 (* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem mode0 ctxt type_lits cls thss =
-  let val thy = Proof_Context.theory_of ctxt
-      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
-      fun set_mode FO = FO
-        | set_mode HO =
-          if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
-          else HO
-        | set_mode FT = FT
-      val mode = set_mode mode0
+fun prepare_metis_problem New ctxt type_lits cls thss =
+    error "Not implemented yet"
+  | prepare_metis_problem mode ctxt type_lits cls thss =
+    let
+      val thy = Proof_Context.theory_of ctxt
+      (* The modes FO and FT are sticky. HO can be downgraded to FO. *)
+      val mode =
+        if mode = HO andalso
+           forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then
+          FO
+        else
+          mode
       (*transform isabelle clause to metis clause *)
       fun add_thm is_conjecture (isa_ith, metis_ith)
                   {axioms, tfrees, old_skolems} : metis_problem =
@@ -338,8 +343,9 @@
                           if needs_full_types andalso mode <> FT then []
                           else map prepare_helper thms)
           in lmap |> fold (add_thm false) helper_ths end
-  in
-    (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
-  end
+    in
+      (mode,
+       add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
+    end
 
 end;