src/HOL/Tools/Nitpick/nitpick.ML
changeset 43020 abb5d1f907e4
parent 42959 ee829022381d
child 43022 7d3ce43d9464
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -55,6 +55,11 @@
     1.4       batch_size: int,
     1.5       expect: string}
     1.6  
     1.7 +  val genuineN : string
     1.8 +  val quasi_genuineN : string
     1.9 +  val potentialN : string
    1.10 +  val noneN : string
    1.11 +  val unknownN : string
    1.12    val register_frac_type : string -> (string * string) list -> theory -> theory
    1.13    val unregister_frac_type : string -> theory -> theory
    1.14    val register_codatatype : typ -> string -> styp list -> theory -> theory
    1.15 @@ -131,6 +136,12 @@
    1.16     batch_size: int,
    1.17     expect: string}
    1.18  
    1.19 +val genuineN = "genuine"
    1.20 +val quasi_genuineN = "quasi_genuine"
    1.21 +val potentialN = "potential"
    1.22 +val noneN = "none"
    1.23 +val unknownN = "unknown"
    1.24 +
    1.25  (* TODO: eliminate these historical aliases *)
    1.26  val register_frac_type = Nitpick_HOL.register_frac_type_global
    1.27  val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global
    1.28 @@ -973,7 +984,7 @@
    1.29      fun run_batches _ _ []
    1.30                      (found_really_genuine, max_potential, max_genuine, donno) =
    1.31          if donno > 0 andalso max_genuine > 0 then
    1.32 -          (print_m (fn () => excipit "checked"); "unknown")
    1.33 +          (print_m (fn () => excipit "checked"); unknownN)
    1.34          else if max_genuine = original_max_genuine then
    1.35            if max_potential = original_max_potential then
    1.36              (print_m (fn () =>
    1.37 @@ -982,7 +993,7 @@
    1.38                      " This suggests that the induction hypothesis might be \
    1.39                      \general enough to prove this subgoal."
    1.40                    else
    1.41 -                    "")); if skipped > 0 then "unknown" else "none")
    1.42 +                    "")); if skipped > 0 then unknownN else noneN)
    1.43            else
    1.44              (print_m (fn () =>
    1.45                   excipit ("could not find a" ^
    1.46 @@ -991,11 +1002,11 @@
    1.47                             else
    1.48                               "ny better " ^ das_wort_model ^ "s.") ^
    1.49                            " It checked"));
    1.50 -             "potential")
    1.51 +             potentialN)
    1.52          else if found_really_genuine then
    1.53 -          "genuine"
    1.54 +          genuineN
    1.55          else
    1.56 -          "quasi_genuine"
    1.57 +          quasi_genuineN
    1.58        | run_batches j n (batch :: batches) z =
    1.59          let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
    1.60            run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
    1.61 @@ -1007,7 +1018,7 @@
    1.62                    (false, max_potential, max_genuine, 0)
    1.63        handle TimeLimit.TimeOut =>
    1.64               (print_m (fn () => excipit "ran out of time after checking");
    1.65 -              if !met_potential > 0 then "potential" else "unknown")
    1.66 +              if !met_potential > 0 then potentialN else unknownN)
    1.67      val _ = print_v (fn () =>
    1.68                  "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
    1.69                  ".")
    1.70 @@ -1026,7 +1037,7 @@
    1.71         ("no_kodkodi", state))
    1.72      else
    1.73        let
    1.74 -        val unknown_outcome = ("unknown", state)
    1.75 +        val unknown_outcome = (unknownN, state)
    1.76          val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    1.77          val outcome as (outcome_code, _) =
    1.78            time_limit (if debug orelse is_none timeout then NONE
    1.79 @@ -1065,7 +1076,7 @@
    1.80      val t = state |> Proof.raw_goal |> #goal |> prop_of
    1.81    in
    1.82      case Logic.count_prems t of
    1.83 -      0 => (Output.urgent_message "No subgoal!"; ("none", state))
    1.84 +      0 => (Output.urgent_message "No subgoal!"; (noneN, state))
    1.85      | n =>
    1.86        let
    1.87          val t = Logic.goal_params t i |> fst