# HG changeset patch
# User blanchet
# Date 1315396217 -7200
# Node ID f4975fa4a2f8bcc7c484e48575ebe7346aafdb4a
# Parent  c9a081ef441d078d747c5d8b38290471be8519e6
parse new experimental '@' encodings

diff -r c9a081ef441d -r f4975fa4a2f8 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -571,11 +571,25 @@
   | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
   | is_type_level_monotonicity_based _ = false
 
+(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
+   Mirabelle. *)
+val queries = ["?", "_query"]
+val bangs = ["!", "_bang"]
+val ats = ["@", "_at"]
+
 fun try_unsuffixes ss s =
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
 
-val queries = ["?", "_query"]
-val bangs = ["!", "_bang"]
+fun try_nonmono constr suffixes fallback s =
+  case try_unsuffixes suffixes s of
+    SOME s =>
+    (case try_unsuffixes suffixes s of
+       SOME s => (constr Ann_Light, s)
+     | NONE =>
+       case try_unsuffixes ats s of
+         SOME s => (constr Arg_Light, s)
+       | NONE => (constr Heavy, s))
+  | NONE => fallback s
 
 fun type_enc_from_string soundness s =
   (case try (unprefix "poly_") s of
@@ -587,21 +601,9 @@
        case try (unprefix "mono_") s of
          SOME s => (SOME Mangled_Monomorphic, s)
        | NONE => (NONE, s))
-  ||> (fn s =>
-          (* "_query" and "_bang" are for the ASCII-challenged Metis and
-             Mirabelle. *)
-          case try_unsuffixes queries s of
-            SOME s =>
-            (case try_unsuffixes queries s of
-               SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s)
-             | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s))
-          | NONE =>
-            case try_unsuffixes bangs s of
-              SOME s =>
-              (case try_unsuffixes bangs s of
-                 SOME s => (Fin_Nonmono_Types Ann_Light, s)
-               | NONE => (Fin_Nonmono_Types Heavy, s))
-            | NONE => (All_Types, s))
+  ||> (pair All_Types
+       |> try_nonmono Fin_Nonmono_Types bangs
+       |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
   |> (fn (poly, (level, core)) =>
          case (core, (poly, level)) of
            ("simple", (SOME poly, _)) =>
@@ -633,7 +635,7 @@
          | ("erased", (NONE, All_Types (* naja *))) =>
            Guards (Polymorphic, No_Types)
          | _ => raise Same.SAME)
-  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
+  handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
 
 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
                     (Simple_Types (order, _, level)) =
diff -r c9a081ef441d -r f4975fa4a2f8 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -575,7 +575,7 @@
         | _ => SOME tab
   in aux (prop_of th) [] end
 
-(* FIXME: This is currently only useful for polymorphic type systems. *)
+(* FIXME: This is currently only useful for polymorphic type encodings. *)
 fun could_benefit_from_ext is_built_in_const facts =
   fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   |> is_none
diff -r c9a081ef441d -r f4975fa4a2f8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -152,8 +152,8 @@
            error ("Unknown parameter: " ^ quote name ^ "."))
 
 
-(* Ensure that type systems such as "mono_simple?" and "poly_guards!!" are
-   handled correctly. *)
+(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are
+   read correctly. *)
 val implode_param = strip_spaces_except_between_idents o space_implode " "
 
 structure Data = Theory_Data