restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
authorblanchet
Sun May 01 18:37:25 2011 +0200 (2011-05-01)
changeset 425899f7c48463645
parent 42588 562d6415616a
child 42590 03834570af86
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -578,57 +578,71 @@
     1.4  Monomorphization can simplify reasoning but also leads to larger fact bases,
     1.5  which can slow down the ATPs.
     1.6  
     1.7 -\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names,
     1.8 -and predicates restrict the range of bound variables. The problem is
     1.9 -monomorphized. This corresponds to the traditional encoding of types in an
    1.10 -untyped logic without overloading (e.g., such as performed by the ToFoF-E
    1.11 -wrapper).
    1.12 +\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate
    1.13 +$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
    1.14 +Constants are annotated with their types, supplied as extra arguments, to
    1.15 +resolve overloading.
    1.16  
    1.17 -\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with their
    1.18 -types, which are supplied as extra arguments.
    1.19 +\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
    1.20 +the problem is additionally monomorphized. This corresponds to the traditional
    1.21 +encoding of types in an untyped logic without overloading (e.g., such as
    1.22 +performed by the ToFoF-E wrapper).
    1.23  
    1.24 -\item[$\bullet$] \textbf{\textit{mono\_args}:} Similar to \textit{args}, but
    1.25 -the problem is additionally monomorphized.
    1.26 +\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
    1.27 +\textit{mono\_preds}, but types are mangled in constant names instead of being
    1.28 +supplied as ground term arguments. The binary predicate
    1.29 +$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
    1.30 +$\mathit{has\_type\_}\tau(t)$.
    1.31  
    1.32 -\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
    1.33 -its type using a special uninterpreted function symbol.
    1.34 +\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
    1.35 +its type using a function $\mathit{type\_info\/}(\tau, t)$.
    1.36  
    1.37  \item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
    1.38  the problem is additionally monomorphized.
    1.39  
    1.40 -\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
    1.41 -ATP.
    1.42 +\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
    1.43 +\textit{mono\_tags}, but types are mangled in constant names instead of being
    1.44 +supplied as ground term arguments. The binary function
    1.45 +$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
    1.46 +$\mathit{type\_info\_}\tau(t)$.
    1.47 +
    1.48 +\item[$\bullet$]
    1.49 +\textbf{%
    1.50 +\textit{preds}!,
    1.51 +\textit{mono\_preds}!,
    1.52 +\textit{mangled\_preds}!, \\
    1.53 +\textit{tags}!,
    1.54 +\textit{mono\_tags}!,
    1.55 +\textit{mangled\_tags}!:} \\
    1.56 +The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
    1.57 +\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
    1.58 +and virtually sound. For each of these, Sledgehammer also provides a mildly
    1.59 +unsound variant identified by an exclamation mark (!)\ that types only finite
    1.60 +(and hence especially dangerous) types.
    1.61  
    1.62  \item[$\bullet$]
    1.63  \textbf{%
    1.64 -\textit{many\_typed}!,
    1.65 -\textit{mangled}!,
    1.66 -\textit{args}!,
    1.67 -\textit{mono\_args}!,
    1.68 -\textit{tags}!, \\ %% TYPESETTING
    1.69 -\textit{mono\_tags}!:}
    1.70 -The type systems \textit{many\_typed}, \textit{mangled},
    1.71 -(\textit{mono\_})\allowbreak\textit{args}, and
    1.72 -(\textit{mono\_})\allowbreak\textit{tags} are fully typed and (virtually) sound.
    1.73 -For each of these, Sledgehammer also provides a mildly unsound variant
    1.74 -identified by one exclamation mark suffix (!).
    1.75 +\textit{preds}?,
    1.76 +\textit{mono\_preds}?,
    1.77 +\textit{mangled\_preds}?, \\
    1.78 +\textit{tags}?,
    1.79 +\textit{mono\_tags}?,
    1.80 +\textit{mangled\_tags}?:} \\
    1.81 +If the exclamation mark (!) is replaced by an question mark (?), the type
    1.82 +systems type only nonmonotonic (and hence especially dangerous) types. Not
    1.83 +implemented yet.
    1.84  
    1.85 -\item[$\bullet$]
    1.86 -\textbf{%
    1.87 -\textit{many\_typed}!!,
    1.88 -\textit{mangled}!!,
    1.89 -\textit{args}!!,
    1.90 -\textit{mono\_args}!!,
    1.91 -\textit{tags}!!, \\ %% TYPESETTING
    1.92 -\textit{mono\_tags}!!:}
    1.93 -More strongly unsound variants of \textit{many\_typed}, \textit{mangled},
    1.94 -(\textit{mono\_})\allowbreak\textit{args}, and
    1.95 -(\textit{mono\_})\allowbreak\textit{tags}, identified by two exclamation marks
    1.96 -(!!).
    1.97 +\item[$\bullet$] \textbf{\textit{const\_args}:}
    1.98 +Constants are annotated with their types, supplied as extra arguments, to
    1.99 +resolve overloading. Variables are unbounded.
   1.100 +
   1.101 +\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
   1.102 +the ATP. Types are simply erased.
   1.103  
   1.104  \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
   1.105 -uses a fully typed encoding; otherwise, uses a partially typed encoding. The
   1.106 -actual encoding used depends on the ATP.
   1.107 +uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
   1.108 +actual encoding used depends on the ATP and should be the most efficient for
   1.109 +that ATP.
   1.110  \end{enum}
   1.111  
   1.112  For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 01 18:37:25 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 01 18:37:25 2011 +0200
     2.3 @@ -377,7 +377,8 @@
     2.4        Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
     2.5      val relevance_override = {add = [], del = [], only = false}
     2.6      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     2.7 -    val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
     2.8 +    val fairly_sound =
     2.9 +      Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
    2.10      val time_limit =
    2.11        (case hard_timeout of
    2.12          NONE => I
    2.13 @@ -387,7 +388,7 @@
    2.14          time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
    2.15        let
    2.16          val facts =
    2.17 -          Sledgehammer_Filter.relevant_facts ctxt half_sound
    2.18 +          Sledgehammer_Filter.relevant_facts ctxt fairly_sound
    2.19                relevance_thresholds
    2.20                (the_default default_max_relevant max_relevant) is_built_in_const
    2.21                relevance_fudge relevance_override chained_ths hyp_ts concl_t
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Sun May 01 18:37:25 2011 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Sun May 01 18:37:25 2011 +0200
     3.3 @@ -117,18 +117,18 @@
     3.4           val default_max_relevant =
     3.5             Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
     3.6                                                                  prover
     3.7 -        val is_built_in_const =
     3.8 -          Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
     3.9 +         val is_built_in_const =
    3.10 +           Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
    3.11           val relevance_fudge =
    3.12             extract_relevance_fudge args
    3.13                 (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
    3.14           val relevance_override = {add = [], del = [], only = false}
    3.15           val subgoal = 1
    3.16           val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
    3.17 -         val half_sound =
    3.18 -           Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
    3.19 +         val fairly_sound =
    3.20 +           Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
    3.21           val facts =
    3.22 -           Sledgehammer_Filter.relevant_facts ctxt half_sound
    3.23 +           Sledgehammer_Filter.relevant_facts ctxt fairly_sound
    3.24                 relevance_thresholds
    3.25                 (the_default default_max_relevant max_relevant) is_built_in_const
    3.26                 relevance_fudge relevance_override facts hyp_ts concl_t
     4.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
     4.3 @@ -164,7 +164,7 @@
     4.4        | keep (c :: cs) = c :: keep cs
     4.5    in String.explode #> rev #> keep #> rev #> String.implode end
     4.6  
     4.7 -val max_readable_name_length = 32
     4.8 +val max_readable_name_length = 24
     4.9  
    4.10  (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
    4.11     problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
    4.12 @@ -184,7 +184,7 @@
    4.13               if size s > max_readable_name_length then
    4.14                 String.substring (s, 0, max_readable_name_length div 2 - 4) ^
    4.15                 Word.toString (hashw_string (full_name, 0w0)) ^
    4.16 -               String.extract (s, max_readable_name_length div 2 - 4, NONE)
    4.17 +               String.extract (s, max_readable_name_length div 2 + 4, NONE)
    4.18               else
    4.19                 s)
    4.20        |> (fn s => if member (op =) reserved_nice_names s then full_name else s)
     5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
     5.3 @@ -11,13 +11,14 @@
     5.4    type formula_kind = ATP_Problem.formula_kind
     5.5    type failure = ATP_Proof.failure
     5.6  
     5.7 -  datatype type_level = Sound | Half_Sound | Unsound
     5.8 +  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
     5.9 +  datatype type_level =
    5.10 +    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    5.11 +
    5.12    datatype type_system =
    5.13      Many_Typed |
    5.14 -    Mangled of type_level |
    5.15 -    Args of bool * type_level |
    5.16 -    Tags of bool * type_level |
    5.17 -    No_Types
    5.18 +    Preds of polymorphism * type_level |
    5.19 +    Tags of polymorphism * type_level
    5.20  
    5.21    type atp_config =
    5.22      {exec : string * string,
    5.23 @@ -33,7 +34,10 @@
    5.24    datatype e_weight_method =
    5.25      E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    5.26  
    5.27 +  val polymorphism_of_type_sys : type_system -> polymorphism
    5.28    val level_of_type_sys : type_system -> type_level
    5.29 +  val is_type_sys_virtually_sound : type_system -> bool
    5.30 +  val is_type_sys_fairly_sound : type_system -> bool
    5.31    (* for experimentation purposes -- do not use in production code *)
    5.32    val e_weight_method : e_weight_method Unsynchronized.ref
    5.33    val e_default_fun_weight : real Unsynchronized.ref
    5.34 @@ -71,19 +75,31 @@
    5.35  
    5.36  (* ATP configuration *)
    5.37  
    5.38 -datatype type_level = Sound | Half_Sound | Unsound
    5.39 +datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    5.40 +datatype type_level =
    5.41 +  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    5.42 +
    5.43  datatype type_system =
    5.44    Many_Typed |
    5.45 -  Mangled of type_level |
    5.46 -  Args of bool * type_level |
    5.47 -  Tags of bool * type_level |
    5.48 -  No_Types
    5.49 +  Preds of polymorphism * type_level |
    5.50 +  Tags of polymorphism * type_level
    5.51 +
    5.52 +fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
    5.53 +  | polymorphism_of_type_sys (Preds (poly, _)) = poly
    5.54 +  | polymorphism_of_type_sys (Tags (poly, _)) = poly
    5.55  
    5.56 -fun level_of_type_sys Many_Typed = Sound
    5.57 -  | level_of_type_sys (Mangled level) = level
    5.58 -  | level_of_type_sys (Args (_, level)) = level
    5.59 +fun level_of_type_sys Many_Typed = All_Types
    5.60 +  | level_of_type_sys (Preds (_, level)) = level
    5.61    | level_of_type_sys (Tags (_, level)) = level
    5.62 -  | level_of_type_sys No_Types = Unsound
    5.63 +
    5.64 +val is_type_level_virtually_sound =
    5.65 +  member (op =) [All_Types, Nonmonotonic_Types]
    5.66 +val is_type_sys_virtually_sound =
    5.67 +  is_type_level_virtually_sound o level_of_type_sys
    5.68 +
    5.69 +fun is_type_level_fairly_sound level =
    5.70 +  is_type_level_virtually_sound level orelse level = Finite_Types
    5.71 +val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
    5.72  
    5.73  type atp_config =
    5.74    {exec : string * string,
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
     6.3 @@ -194,7 +194,7 @@
     6.4    | using_labels ls =
     6.5      "using " ^ space_implode " " (map string_for_label ls) ^ " "
     6.6  fun metis_name type_sys =
     6.7 -  if level_of_type_sys type_sys = Unsound then "metis" else "metisFT"
     6.8 +  if is_type_sys_fairly_sound type_sys then "metisFT" else "metis"
     6.9  fun metis_call type_sys ss = command_call (metis_name type_sys) ss
    6.10  fun metis_command type_sys i n (ls, ss) =
    6.11    using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
    6.12 @@ -342,12 +342,7 @@
    6.13      fun aux opt_T extra_us u =
    6.14        case u of
    6.15          ATerm (a, us) =>
    6.16 -        if a = type_tag_name then
    6.17 -          case us of
    6.18 -            [typ_u, term_u] =>
    6.19 -            aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
    6.20 -          | _ => raise FO_TERM us
    6.21 -        else if String.isPrefix tff_type_prefix a then
    6.22 +        if String.isPrefix tff_type_prefix a then
    6.23            @{const True} (* ignore TFF type information *)
    6.24          else case strip_prefix_and_unascii const_prefix a of
    6.25            SOME "equal" =>
    6.26 @@ -360,7 +355,12 @@
    6.27            end
    6.28          | SOME b =>
    6.29            let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
    6.30 -            if b = predicator_base then
    6.31 +            if b = type_tag_name then
    6.32 +              case mangled_us @ us of
    6.33 +                [typ_u, term_u] =>
    6.34 +                aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
    6.35 +              | _ => raise FO_TERM us
    6.36 +            else if b = predicator_base then
    6.37                aux (SOME @{typ bool}) [] (hd us)
    6.38              else if b = explicit_app_base then
    6.39                aux opt_T (nth us 1 :: extra_us) (hd us)
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     7.3 @@ -42,7 +42,9 @@
     7.4  open Sledgehammer_Util
     7.5  
     7.6  (* Readable names are often much shorter, especially if types are mangled in
     7.7 -   names. For that reason, they are on by default. *)
     7.8 +   names. Also, the logic for generating legal SNARK sort names is only
     7.9 +   implemented for readable names. Finally, readable names are, well, more
    7.10 +   readable. For these reason, they are enabled by default. *)
    7.11  val readable_names = Unsynchronized.ref true
    7.12  
    7.13  val type_decl_prefix = "type_"
    7.14 @@ -91,29 +93,25 @@
    7.15  
    7.16  fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
    7.17  
    7.18 -fun type_sys_declares_sym_types Many_Typed = true
    7.19 -  | type_sys_declares_sym_types (Mangled level) = level <> Unsound
    7.20 -  | type_sys_declares_sym_types (Args (_, level)) = level <> Unsound
    7.21 -  | type_sys_declares_sym_types _ = false
    7.22 -
    7.23  val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
    7.24  
    7.25  fun should_omit_type_args type_sys s =
    7.26 -  s <> type_pred_base andalso
    7.27 -  (s = @{const_name HOL.eq} orelse
    7.28 -   case type_sys of
    7.29 -     Many_Typed => false
    7.30 -   | Mangled _ => false
    7.31 -   | Tags (_, Sound) => true
    7.32 -   | No_Types => true
    7.33 -   | _ => member (op =) boring_consts s)
    7.34 +  s <> type_pred_base andalso s <> type_tag_name andalso
    7.35 +  (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
    7.36 +   (case type_sys of
    7.37 +      Tags (_, All_Types) => true
    7.38 +    | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
    7.39 +           member (op =) boring_consts s))
    7.40 +  
    7.41 +datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
    7.42  
    7.43 -datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args
    7.44 -
    7.45 -fun general_type_arg_policy Many_Typed = Mangled_Types
    7.46 -  | general_type_arg_policy (Mangled _) = Mangled_Types
    7.47 -  | general_type_arg_policy No_Types = No_Type_Args
    7.48 -  | general_type_arg_policy _ = Explicit_Type_Args
    7.49 +fun general_type_arg_policy type_sys =
    7.50 +  if level_of_type_sys type_sys = No_Types then
    7.51 +    No_Type_Args
    7.52 +  else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
    7.53 +    Mangled_Type_Args
    7.54 +  else
    7.55 +    Explicit_Type_Args
    7.56  
    7.57  fun type_arg_policy type_sys s =
    7.58    if should_omit_type_args type_sys s then No_Type_Args
    7.59 @@ -124,7 +122,7 @@
    7.60    else 0
    7.61  
    7.62  fun atp_type_literals_for_types type_sys kind Ts =
    7.63 -  if type_sys = No_Types then
    7.64 +  if level_of_type_sys type_sys = No_Types then
    7.65      []
    7.66    else
    7.67      Ts |> type_literals_for_types
    7.68 @@ -486,8 +484,8 @@
    7.69             let val s'' = invert_const s'' in
    7.70               case type_arg_policy type_sys s'' of
    7.71                 No_Type_Args => (name, [])
    7.72 -             | Mangled_Types => (mangled_const_name T_args name, [])
    7.73               | Explicit_Type_Args => (name, T_args)
    7.74 +             | Mangled_Type_Args => (mangled_const_name T_args name, [])
    7.75             end)
    7.76          |> (fn (name, T_args) => CombConst (name, T, T_args))
    7.77        | aux tm = tm
    7.78 @@ -504,7 +502,7 @@
    7.79  fun ti_ti_helper_fact () =
    7.80    let
    7.81      fun var s = ATerm (`I s, [])
    7.82 -    fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
    7.83 +    fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
    7.84    in
    7.85      Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
    7.86               AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
    7.87 @@ -521,7 +519,7 @@
    7.88          ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
    7.89            false),
    7.90           let val t = th |> prop_of in
    7.91 -           t |> (general_type_arg_policy type_sys = Mangled_Types andalso
    7.92 +           t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
    7.93                   not (null (Term.hidden_polymorphism t)))
    7.94                  ? (case typ of
    7.95                       SOME T => specialize_type thy (invert_const unmangled_s, T)
    7.96 @@ -529,12 +527,12 @@
    7.97           end)
    7.98        fun make_facts eq_as_iff =
    7.99          map_filter (make_fact ctxt false eq_as_iff false)
   7.100 +      val has_some_types = is_type_sys_fairly_sound type_sys
   7.101      in
   7.102        metis_helpers
   7.103        |> maps (fn (metis_s, (needs_some_types, ths)) =>
   7.104                    if metis_s <> unmangled_s orelse
   7.105 -                     (needs_some_types andalso
   7.106 -                      level_of_type_sys type_sys = Unsound) then
   7.107 +                     (needs_some_types andalso not has_some_types) then
   7.108                      []
   7.109                    else
   7.110                      ths ~~ (1 upto length ths)
   7.111 @@ -567,15 +565,13 @@
   7.112      val tycons = type_consts_of_terms thy all_ts
   7.113      val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
   7.114      val (supers', arity_clauses) =
   7.115 -      if type_sys = No_Types then ([], [])
   7.116 +      if level_of_type_sys type_sys = No_Types then ([], [])
   7.117        else make_arity_clauses thy tycons supers
   7.118      val class_rel_clauses = make_class_rel_clauses thy subs supers'
   7.119    in
   7.120      (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   7.121    end
   7.122  
   7.123 -fun tag_with_type ty tm = ATerm (`I type_tag_name, [ty, tm])
   7.124 -
   7.125  fun fo_literal_from_type_literal (TyLitVar (class, name)) =
   7.126      (true, ATerm (class, [ATerm (name, [])]))
   7.127    | fo_literal_from_type_literal (TyLitFree (class, name)) =
   7.128 @@ -588,39 +584,39 @@
   7.129     unsound ATP proofs. The checks below are an (unsound) approximation of
   7.130     finiteness. *)
   7.131  
   7.132 -fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true
   7.133 -  | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) =
   7.134 -    is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us
   7.135 -  | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
   7.136 -and is_type_dangerous ctxt (Type (s, Ts)) =
   7.137 -    is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
   7.138 -  | is_type_dangerous _ _ = false
   7.139 -and is_type_constr_dangerous ctxt s =
   7.140 +fun is_dtyp_finite _ (Datatype_Aux.DtTFree _) = true
   7.141 +  | is_dtyp_finite ctxt (Datatype_Aux.DtType (s, Us)) =
   7.142 +    is_type_constr_finite ctxt s andalso forall (is_dtyp_finite ctxt) Us
   7.143 +  | is_dtyp_finite _ (Datatype_Aux.DtRec _) = false
   7.144 +and is_type_finite ctxt (Type (s, Ts)) =
   7.145 +    is_type_constr_finite ctxt s andalso forall (is_type_finite ctxt) Ts
   7.146 +  | is_type_finite _ _ = false
   7.147 +and is_type_constr_finite ctxt s =
   7.148    let val thy = Proof_Context.theory_of ctxt in
   7.149      case Datatype_Data.get_info thy s of
   7.150        SOME {descr, ...} =>
   7.151        forall (fn (_, (_, _, constrs)) =>
   7.152 -                 forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr
   7.153 +                 forall (forall (is_dtyp_finite ctxt) o snd) constrs) descr
   7.154      | NONE =>
   7.155        case Typedef.get_info ctxt s of
   7.156 -        ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type
   7.157 +        ({rep_type, ...}, _) :: _ => is_type_finite ctxt rep_type
   7.158        | [] => true
   7.159    end
   7.160  
   7.161 -fun should_encode_type _ Sound _ = true
   7.162 -  | should_encode_type ctxt Half_Sound T = is_type_dangerous ctxt T
   7.163 -  | should_encode_type _ Unsound _ = false
   7.164 +fun should_encode_type _ All_Types _ = true
   7.165 +  | should_encode_type ctxt Finite_Types T = is_type_finite ctxt T
   7.166 +  | should_encode_type _ Nonmonotonic_Types _ =
   7.167 +    error "Monotonicity inference not implemented yet."
   7.168 +  | should_encode_type _ _ _ = false
   7.169 +
   7.170 +fun should_predicate_on_type ctxt (Preds (_, level)) T =
   7.171 +    should_encode_type ctxt level T
   7.172 +  | should_predicate_on_type _ _ _ = false
   7.173  
   7.174  fun should_tag_with_type ctxt (Tags (_, level)) T =
   7.175      should_encode_type ctxt level T
   7.176    | should_tag_with_type _ _ _ = false
   7.177  
   7.178 -fun should_predicate_on_type ctxt (Mangled level) T =
   7.179 -    should_encode_type ctxt level T
   7.180 -  | should_predicate_on_type ctxt (Args (_, level)) T =
   7.181 -    should_encode_type ctxt level T
   7.182 -  | should_predicate_on_type _ _ _ = false
   7.183 -
   7.184  fun type_pred_combatom type_sys T tm =
   7.185    CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
   7.186             tm)
   7.187 @@ -629,7 +625,12 @@
   7.188  
   7.189  fun formula_from_combformula ctxt type_sys =
   7.190    let
   7.191 -    fun do_term top_level u =
   7.192 +    fun tag_with_type type_sys T tm =
   7.193 +      CombConst (`make_fixed_const type_tag_name, T --> T, [T])
   7.194 +      |> impose_type_arg_policy_in_combterm type_sys
   7.195 +      |> do_term true
   7.196 +      |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
   7.197 +    and do_term top_level u =
   7.198        let
   7.199          val (head, args) = strip_combterm_comb u
   7.200          val (x, T_args) =
   7.201 @@ -642,7 +643,7 @@
   7.202          val T = combtyp_of u
   7.203        in
   7.204          t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then
   7.205 -                tag_with_type (fo_term_from_typ T)
   7.206 +                tag_with_type type_sys T
   7.207                else
   7.208                  I)
   7.209        end
   7.210 @@ -735,7 +736,7 @@
   7.211    let
   7.212      fun declare_sym (decl as (_, _, T, _, _)) decls =
   7.213        case type_sys of
   7.214 -        Tags (false, Sound) =>
   7.215 +        Preds (Polymorphic, All_Types) =>
   7.216          if exists (curry Type.raw_instance T o #3) decls then
   7.217            decls
   7.218          else
   7.219 @@ -760,7 +761,7 @@
   7.220    fact_lift (formula_fold
   7.221        (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))
   7.222  fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
   7.223 -  Symtab.empty |> type_sys_declares_sym_types type_sys
   7.224 +  Symtab.empty |> is_type_sys_fairly_sound type_sys
   7.225                    ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
   7.226                           facts
   7.227  
   7.228 @@ -787,10 +788,8 @@
   7.229        bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
   7.230      val bound_Ts =
   7.231        arg_Ts |> map (if n > 1 then SOME else K NONE)
   7.232 -    val freshener =
   7.233 -      case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
   7.234    in
   7.235 -    Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
   7.236 +    Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
   7.237               CombConst ((s, s'), T, T_args)
   7.238               |> fold (curry (CombApp o swap)) bound_tms
   7.239               |> type_pred_combatom type_sys res_T
   7.240 @@ -884,7 +883,9 @@
   7.241         (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys)
   7.242                        (0 upto length helpers - 1 ~~ helpers)
   7.243                    |> (case type_sys of
   7.244 -                        Tags (_, Half_Sound) => cons (ti_ti_helper_fact ())
   7.245 +                        Tags (Polymorphic, level) =>
   7.246 +                        member (op =) [Finite_Types, Nonmonotonic_Types] level
   7.247 +                        ? cons (ti_ti_helper_fact ())
   7.248                        | _ => I)),
   7.249         (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
   7.250         (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun May 01 18:37:25 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun May 01 18:37:25 2011 +0200
     8.3 @@ -777,17 +777,17 @@
     8.4  (* Facts containing variables of type "unit" or "bool" or of the form
     8.5     "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
     8.6     are omitted. *)
     8.7 -fun is_dangerous_term half_sound t =
     8.8 -  not half_sound andalso
     8.9 +fun is_dangerous_term fairly_sound t =
    8.10 +  not fairly_sound andalso
    8.11    let val t = transform_elim_term t in
    8.12      has_bound_or_var_of_type dangerous_types t orelse
    8.13      is_exhaustive_finite t
    8.14    end
    8.15  
    8.16 -fun is_theorem_bad_for_atps half_sound thm =
    8.17 +fun is_theorem_bad_for_atps fairly_sound thm =
    8.18    let val t = prop_of thm in
    8.19      is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    8.20 -    is_dangerous_term half_sound t orelse exists_sledgehammer_const t orelse
    8.21 +    is_dangerous_term fairly_sound t orelse exists_sledgehammer_const t orelse
    8.22      exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
    8.23      is_that_fact thm
    8.24    end
    8.25 @@ -800,7 +800,7 @@
    8.26      val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
    8.27    in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
    8.28  
    8.29 -fun all_facts ctxt reserved really_all half_sound
    8.30 +fun all_facts ctxt reserved really_all fairly_sound
    8.31                ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
    8.32                add_ths chained_ths =
    8.33    let
    8.34 @@ -846,7 +846,7 @@
    8.35              pair 1
    8.36              #> fold (fn th => fn (j, rest) =>
    8.37                   (j + 1,
    8.38 -                  if is_theorem_bad_for_atps half_sound th andalso
    8.39 +                  if is_theorem_bad_for_atps fairly_sound th andalso
    8.40                       not (member Thm.eq_thm add_ths th) then
    8.41                      rest
    8.42                    else
    8.43 @@ -890,7 +890,7 @@
    8.44  fun external_frees t =
    8.45    [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
    8.46  
    8.47 -fun relevant_facts ctxt half_sound (threshold0, threshold1) max_relevant
    8.48 +fun relevant_facts ctxt fairly_sound (threshold0, threshold1) max_relevant
    8.49                     is_built_in_const fudge (override as {add, only, ...})
    8.50                     chained_ths hyp_ts concl_t =
    8.51    let
    8.52 @@ -908,7 +908,7 @@
    8.53           maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
    8.54                 o fact_from_ref ctxt reserved chained_ths) add
    8.55         else
    8.56 -         all_facts ctxt reserved false half_sound fudge add_ths chained_ths)
    8.57 +         all_facts ctxt reserved false fairly_sound fudge add_ths chained_ths)
    8.58        |> instantiate_inducts
    8.59           ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
    8.60        |> rearrange_facts ctxt (respect_no_atp andalso not only)
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:25 2011 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:25 2011 +0200
     9.3 @@ -235,22 +235,29 @@
     9.4                    |> auto ? single o hd
     9.5      val type_sys = lookup_string "type_sys"
     9.6      val type_sys =
     9.7 -      (case try (unprefix "mono_") type_sys of
     9.8 -         SOME s => (true, s)
     9.9 -       | NONE => (false, type_sys))
    9.10 -      ||> (fn s => case try (unsuffix " !!") s of
    9.11 -                     SOME s => (Unsound, s)
    9.12 -                   | NONE => case try (unsuffix " !") s of
    9.13 -                               SOME s => (Half_Sound, s)
    9.14 -                             | NONE => (Sound, s))
    9.15 -      |> (fn (mono, (level, core)) =>
    9.16 -             case (core, (mono, level)) of
    9.17 -               ("many_typed", (false, Sound)) => Dumb_Type_Sys Many_Typed
    9.18 -             | ("mangled", (false, level)) => Dumb_Type_Sys (Mangled level)
    9.19 -             | ("args", extra) => Dumb_Type_Sys (Args extra)
    9.20 +      (case try (unprefix "mangled_") type_sys of
    9.21 +         SOME s => (Mangled_Monomorphic, s)
    9.22 +       | NONE =>
    9.23 +         case try (unprefix "mono_") type_sys of
    9.24 +           SOME s => (Monomorphic, s)
    9.25 +         | NONE => (Polymorphic, type_sys))
    9.26 +      ||> (fn s => case try (unsuffix " ?") s of
    9.27 +                     SOME s => (Nonmonotonic_Types, s)
    9.28 +                   | NONE =>
    9.29 +                     case try (unsuffix " !") s of
    9.30 +                       SOME s => (Finite_Types, s)
    9.31 +                     | NONE => (All_Types, s))
    9.32 +      |> (fn (polymorphism, (level, core)) =>
    9.33 +             case (core, (polymorphism, level)) of
    9.34 +               ("many_typed", (Polymorphic (* naja *), All_Types)) =>
    9.35 +               Dumb_Type_Sys Many_Typed
    9.36 +             | ("preds", extra) => Dumb_Type_Sys (Preds extra)
    9.37               | ("tags", extra) => Dumb_Type_Sys (Tags extra)
    9.38 -             | ("none", (false, Sound)) => Dumb_Type_Sys No_Types
    9.39 -             | ("smart", (false, Sound)) =>
    9.40 +             | ("const_args", (_, All_Types (* naja *))) =>
    9.41 +               Dumb_Type_Sys (Preds (polymorphism, Const_Arg_Types))
    9.42 +             | ("erased", (Polymorphic, All_Types (* naja *))) =>
    9.43 +               Dumb_Type_Sys (Preds (polymorphism, No_Types))
    9.44 +             | ("smart", (Polymorphic, All_Types) (* naja *)) =>
    9.45                 Smart_Type_Sys (lookup_bool "full_types")
    9.46               | _ => error ("Unknown type system: " ^ quote type_sys ^ "."))
    9.47      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    9.48 @@ -351,7 +358,7 @@
    9.49  
    9.50  val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
    9.51  val parse_value =
    9.52 -  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "!!"
    9.53 +  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
    9.54                  || Parse.$$$ "!")
    9.55  val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
    9.56  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
    10.3 @@ -86,7 +86,7 @@
    10.4    val weight_smt_fact :
    10.5      theory -> int -> ((string * locality) * thm) * int
    10.6      -> (string * locality) * (int option * thm)
    10.7 -  val is_rich_type_sys_half_sound : rich_type_system -> bool
    10.8 +  val is_rich_type_sys_fairly_sound : rich_type_system -> bool
    10.9    val untranslated_fact : prover_fact -> (string * locality) * thm
   10.10    val smt_weighted_fact :
   10.11      theory -> int -> prover_fact * int
   10.12 @@ -313,9 +313,9 @@
   10.13  fun weight_smt_fact thy num_facts ((info, th), j) =
   10.14    (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
   10.15  
   10.16 -fun is_rich_type_sys_half_sound (Dumb_Type_Sys type_sys) =
   10.17 -    level_of_type_sys type_sys <> Unsound
   10.18 -  | is_rich_type_sys_half_sound (Smart_Type_Sys full_types) = full_types
   10.19 +fun is_rich_type_sys_fairly_sound (Dumb_Type_Sys type_sys) =
   10.20 +    is_type_sys_fairly_sound type_sys
   10.21 +  | is_rich_type_sys_fairly_sound (Smart_Type_Sys full_types) = full_types
   10.22  
   10.23  fun untranslated_fact (Untranslated_Fact p) = p
   10.24    | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
   10.25 @@ -339,17 +339,12 @@
   10.26     them each time. *)
   10.27  val atp_important_message_keep_factor = 0.1
   10.28  
   10.29 -fun type_sys_monomorphizes Many_Typed = true
   10.30 -  | type_sys_monomorphizes (Mangled _) = true
   10.31 -  | type_sys_monomorphizes (Args (mono, _)) = mono
   10.32 -  | type_sys_monomorphizes (Tags (mono, _)) = mono
   10.33 -  | type_sys_monomorphizes No_Types = false
   10.34 -
   10.35 -val fallback_best_type_systems = [Args (false, Unsound), Many_Typed]
   10.36 +val fallback_best_type_systems =
   10.37 +  [Preds (Polymorphic, Const_Arg_Types), Many_Typed]
   10.38  
   10.39  fun adjust_dumb_type_sys formats Many_Typed =
   10.40      if member (op =) formats Tff then (Tff, Many_Typed)
   10.41 -    else (Fof, Mangled Sound)
   10.42 +    else (Fof, Preds (Mangled_Monomorphic, All_Types))
   10.43    | adjust_dumb_type_sys formats type_sys =
   10.44      if member (op =) formats Fof then (Fof, type_sys)
   10.45      else (Tff, Many_Typed)
   10.46 @@ -358,8 +353,8 @@
   10.47    | determine_format_and_type_sys best_type_systems formats
   10.48                                    (Smart_Type_Sys full_types) =
   10.49      best_type_systems @ fallback_best_type_systems
   10.50 -    |> full_types ? filter (curry (op =) Sound o level_of_type_sys)
   10.51 -    |> hd |> adjust_dumb_type_sys formats
   10.52 +    |> find_first (if full_types then is_type_sys_virtually_sound else K true)
   10.53 +    |> the |> adjust_dumb_type_sys formats
   10.54  
   10.55  fun run_atp auto name
   10.56          ({exec, required_execs, arguments, proof_delims, known_failures,
   10.57 @@ -443,7 +438,8 @@
   10.58                          |> not (null blacklist)
   10.59                             ? filter_out (member (op =) blacklist o fst
   10.60                                           o untranslated_fact)
   10.61 -                        |> type_sys_monomorphizes type_sys ? monomorphize_facts
   10.62 +                        |> polymorphism_of_type_sys type_sys <> Polymorphic
   10.63 +                           ? monomorphize_facts
   10.64                          |> map (atp_translated_fact ctxt)
   10.65                  val real_ms = Real.fromInt o Time.toMilliseconds
   10.66                  val slice_timeout =
   10.67 @@ -507,7 +503,7 @@
   10.68                      NONE =>
   10.69                      if is_unsound_proof conjecture_shape facts_offset fact_names
   10.70                                          atp_proof then
   10.71 -                      SOME (UnsoundProof (level_of_type_sys type_sys = Sound))
   10.72 +                      SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))
   10.73                      else
   10.74                        NONE
   10.75                    | SOME Unprovable =>
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 01 18:37:25 2011 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 01 18:37:25 2011 +0200
    11.3 @@ -183,7 +183,7 @@
    11.4        val thy = Proof_Context.theory_of ctxt
    11.5        val {facts = chained_ths, goal, ...} = Proof.goal state
    11.6        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    11.7 -      val half_sound = is_rich_type_sys_half_sound type_sys
    11.8 +      val fairly_sound = is_rich_type_sys_fairly_sound type_sys
    11.9        val _ = () |> not blocking ? kill_provers
   11.10        val _ = case find_first (not o is_prover_supported ctxt) provers of
   11.11                  SOME name => error ("No such prover: " ^ name ^ ".")
   11.12 @@ -212,7 +212,7 @@
   11.13              |> (if blocking then smart_par_list_map else map) (launch problem)
   11.14              |> exists fst |> rpair state
   11.15          end
   11.16 -      fun get_facts label half_sound relevance_fudge provers =
   11.17 +      fun get_facts label fairly_sound relevance_fudge provers =
   11.18          let
   11.19            val max_max_relevant =
   11.20              case max_relevant of
   11.21 @@ -225,7 +225,7 @@
   11.22            val is_built_in_const =
   11.23              is_built_in_const_for_prover ctxt (hd provers)
   11.24          in
   11.25 -          relevant_facts ctxt half_sound relevance_thresholds max_max_relevant
   11.26 +          relevant_facts ctxt fairly_sound relevance_thresholds max_max_relevant
   11.27                           is_built_in_const relevance_fudge relevance_override
   11.28                           chained_ths hyp_ts concl_t
   11.29            |> tap (fn facts =>
   11.30 @@ -246,7 +246,7 @@
   11.31            accum
   11.32          else
   11.33            launch_provers state
   11.34 -              (get_facts "ATP" half_sound atp_relevance_fudge o K atps)
   11.35 +              (get_facts "ATP" fairly_sound atp_relevance_fudge o K atps)
   11.36                (K (Untranslated_Fact o fst)) (K (K NONE)) atps
   11.37        fun launch_smts accum =
   11.38          if null smts then
    12.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Sun May 01 18:37:25 2011 +0200
    12.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Sun May 01 18:37:25 2011 +0200
    12.3 @@ -32,9 +32,10 @@
    12.4        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    12.5      val relevance_override = {add = [], del = [], only = false}
    12.6      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    12.7 -    val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
    12.8 +    val fairly_sound =
    12.9 +      Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
   12.10      val facts =
   12.11 -      Sledgehammer_Filter.relevant_facts ctxt half_sound relevance_thresholds
   12.12 +      Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds
   12.13            (the_default default_max_relevant max_relevant) is_built_in_const
   12.14            relevance_fudge relevance_override chained_ths hyp_ts concl_t
   12.15      val problem =