src/HOL/Tools/ATP/atp_translate.ML
changeset 44785 f4975fa4a2f8
parent 44783 3634c6dba23f
child 44786 815afb08c079
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -571,11 +571,25 @@
     1.4    | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
     1.5    | is_type_level_monotonicity_based _ = false
     1.6  
     1.7 +(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
     1.8 +   Mirabelle. *)
     1.9 +val queries = ["?", "_query"]
    1.10 +val bangs = ["!", "_bang"]
    1.11 +val ats = ["@", "_at"]
    1.12 +
    1.13  fun try_unsuffixes ss s =
    1.14    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    1.15  
    1.16 -val queries = ["?", "_query"]
    1.17 -val bangs = ["!", "_bang"]
    1.18 +fun try_nonmono constr suffixes fallback s =
    1.19 +  case try_unsuffixes suffixes s of
    1.20 +    SOME s =>
    1.21 +    (case try_unsuffixes suffixes s of
    1.22 +       SOME s => (constr Ann_Light, s)
    1.23 +     | NONE =>
    1.24 +       case try_unsuffixes ats s of
    1.25 +         SOME s => (constr Arg_Light, s)
    1.26 +       | NONE => (constr Heavy, s))
    1.27 +  | NONE => fallback s
    1.28  
    1.29  fun type_enc_from_string soundness s =
    1.30    (case try (unprefix "poly_") s of
    1.31 @@ -587,21 +601,9 @@
    1.32         case try (unprefix "mono_") s of
    1.33           SOME s => (SOME Mangled_Monomorphic, s)
    1.34         | NONE => (NONE, s))
    1.35 -  ||> (fn s =>
    1.36 -          (* "_query" and "_bang" are for the ASCII-challenged Metis and
    1.37 -             Mirabelle. *)
    1.38 -          case try_unsuffixes queries s of
    1.39 -            SOME s =>
    1.40 -            (case try_unsuffixes queries s of
    1.41 -               SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s)
    1.42 -             | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s))
    1.43 -          | NONE =>
    1.44 -            case try_unsuffixes bangs s of
    1.45 -              SOME s =>
    1.46 -              (case try_unsuffixes bangs s of
    1.47 -                 SOME s => (Fin_Nonmono_Types Ann_Light, s)
    1.48 -               | NONE => (Fin_Nonmono_Types Heavy, s))
    1.49 -            | NONE => (All_Types, s))
    1.50 +  ||> (pair All_Types
    1.51 +       |> try_nonmono Fin_Nonmono_Types bangs
    1.52 +       |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
    1.53    |> (fn (poly, (level, core)) =>
    1.54           case (core, (poly, level)) of
    1.55             ("simple", (SOME poly, _)) =>
    1.56 @@ -633,7 +635,7 @@
    1.57           | ("erased", (NONE, All_Types (* naja *))) =>
    1.58             Guards (Polymorphic, No_Types)
    1.59           | _ => raise Same.SAME)
    1.60 -  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    1.61 +  handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
    1.62  
    1.63  fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
    1.64                      (Simple_Types (order, _, level)) =