# HG changeset patch
# User blanchet
# Date 1291637905 -3600
# Node ID f7af68bfa66db65307563023f63dc0c32cfa061b
# Parent  7d52af07bff1ee9a7f509d5a3c05b931e3594f6c
tuning

diff -r 7d52af07bff1 -r f7af68bfa66d src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
@@ -109,9 +109,9 @@
            "_"
          else case M of
              MAlpha => "\<alpha>"
-           | MFun (M1, a, M2) =>
+           | MFun (M1, aa, M2) =>
              aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
-             string_for_annotation_atom a ^ "\<^esup> " ^ aux prec M2
+             string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec M2
            | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
            | MType (s, []) =>
              if s = @{type_name prop} orelse s = @{type_name bool} then "o"
@@ -141,16 +141,16 @@
         (if need_parens then "(" else "") ^
         (case m of
            MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
-         | MAbs (s, _, M, a, m) =>
+         | MAbs (s, _, M, aa, m) =>
            "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
-           string_for_annotation_atom a ^ "\<^esup> " ^ aux prec m
+           string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec m
          | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
         (if need_parens then ")" else "")
       end
   in aux 0 end
 
 fun mtype_of_mterm (MRaw (_, M)) = M
-  | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
+  | mtype_of_mterm (MAbs (_, _, M, aa, m)) = MFun (M, aa, mtype_of_mterm m)
   | mtype_of_mterm (MApp (m1, _)) =
     case mtype_of_mterm m1 of
       MFun (_, _, M12) => M12
@@ -196,8 +196,8 @@
   fold_rev (fn M => curry3 MFun M (A Gen)) Ms (MRec z)
 
 fun repair_mtype _ _ MAlpha = MAlpha
-  | repair_mtype cache seen (MFun (M1, a, M2)) =
-    MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
+  | repair_mtype cache seen (MFun (M1, aa, M2)) =
+    MFun (repair_mtype cache seen M1, aa, repair_mtype cache seen M2)
   | repair_mtype cache seen (MPair Mp) =
     MPair (pairself (repair_mtype cache seen) Mp)
   | repair_mtype cache seen (MType (s, Ms)) =
@@ -246,12 +246,12 @@
   let
     val M1 = fresh_mtype_for_type mdata all_minus T1
     val M2 = fresh_mtype_for_type mdata all_minus T2
-    val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
-               is_fin_fun_supported_type (body_type T2) then
-              V (Unsynchronized.inc max_fresh)
-            else
-              A Gen
-  in (M1, a, M2) end
+    val aa = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
+                is_fin_fun_supported_type (body_type T2) then
+               V (Unsynchronized.inc max_fresh)
+             else
+               A Gen
+  in (M1, aa, M2) end
 and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
                                     datatype_mcache, constr_mcache, ...})
                          all_minus =
@@ -333,12 +333,12 @@
 
 fun resolve_annotation_atom lits (V x) =
     x |> AList.lookup (op =) lits |> Option.map A |> the_default (V x)
-  | resolve_annotation_atom _ a = a
+  | resolve_annotation_atom _ aa = aa
 fun resolve_mtype lits =
   let
     fun aux MAlpha = MAlpha
-      | aux (MFun (M1, a, M2)) =
-        MFun (aux M1, resolve_annotation_atom lits a, aux M2)
+      | aux (MFun (M1, aa, M2)) =
+        MFun (aux M1, resolve_annotation_atom lits aa, aux M2)
       | aux (MPair Mp) = MPair (pairself aux Mp)
       | aux (MType (s, Ms)) = MType (s, map aux Ms)
       | aux (MRec z) = MRec z
@@ -364,35 +364,35 @@
       SOME a' => if a = a' then SOME lits else NONE
     | NONE => SOME ((x, a) :: lits)
 
-fun do_annotation_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
-    (case (a1, a2) of
-       (A sn1, A sn2) => if sn1 = sn2 then SOME accum else NONE
-     | (V x1, A sn2) =>
-       Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits))
-     | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps)
-     | _ => do_annotation_atom_comp Eq [] a2 a1 accum)
-  | do_annotation_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
-    (case (a1, a2) of
+fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (lits, comps)) =
+    (case (aa1, aa2) of
+       (A a1, A a2) => if a1 = a2 then SOME accum else NONE
+     | (V x1, A a2) =>
+       SOME lits |> do_literal (x1, a2) |> Option.map (rpair comps)
+     | (V _, V _) => SOME (lits, insert (op =) (aa1, aa2, Eq, []) comps)
+     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
+  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (lits, comps)) =
+    (case (aa1, aa2) of
        (_, A Gen) => SOME accum
      | (A Fls, _) => SOME accum
      | (A Gen, A Fls) => NONE
-     | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
-     | _ => do_annotation_atom_comp Eq [] a1 a2 accum)
-  | do_annotation_atom_comp cmp xs a1 a2 (lits, comps) =
-    SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
+     | (V _, V _) => SOME (lits, insert (op =) (aa1, aa2, Leq, []) comps)
+     | _ => do_annotation_atom_comp Eq [] aa1 aa2 accum)
+  | do_annotation_atom_comp cmp xs aa1 aa2 (lits, comps) =
+    SOME (lits, insert (op =) (aa1, aa2, cmp, xs) comps)
 
 fun do_mtype_comp _ _ _ _ NONE = NONE
   | do_mtype_comp _ _ MAlpha MAlpha accum = accum
-  | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
+  | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
                   (SOME accum) =
-     accum |> do_annotation_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
-           |> do_mtype_comp Eq xs M12 M22
-  | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
+     accum |> do_annotation_atom_comp Eq xs aa1 aa2
+           |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
+  | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
                   (SOME accum) =
     (if exists_alpha_sub_mtype M11 then
-       accum |> do_annotation_atom_comp Leq xs a1 a2
+       accum |> do_annotation_atom_comp Leq xs aa1 aa2
              |> do_mtype_comp Leq xs M21 M11
-             |> (case a2 of
+             |> (case aa2 of
                    A Gen => I
                  | A Fls => do_mtype_comp Leq xs M11 M21
                  | V x => do_mtype_comp Leq (x :: xs) M11 M21)
@@ -427,10 +427,10 @@
     SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
     SOME (lits, insert (op =) sexp sexps)
-  | do_notin_mtype_fv sn sexp (MFun (M1, A a, M2)) accum =
-    accum |> (if a = Fls andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
+  | do_notin_mtype_fv sn sexp (MFun (M1, A aa, M2)) accum =
+    accum |> (if aa = Fls andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
               else I)
-          |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus sexp M1
+          |> (if aa = Gen orelse sn = Plus then do_notin_mtype_fv Minus sexp M1
               else I)
           |> do_notin_mtype_fv sn sexp M2
   | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
@@ -484,14 +484,14 @@
 fun prop_for_annotation_expr xs = PropLogic.exists (map prop_for_literal xs)
 fun prop_for_exists_eq xs a =
   PropLogic.exists (map (fn x => prop_for_literal (x, a)) xs)
-fun prop_for_comp (a1, a2, Eq, []) =
-    PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
-                    prop_for_comp (a2, a1, Leq, []))
-  | prop_for_comp (a1, a2, Leq, []) =
-    PropLogic.SOr (prop_for_annotation_atom_eq (a1, Fls),
-                   prop_for_annotation_atom_eq (a2, Gen))
-  | prop_for_comp (a1, a2, cmp, xs) =
-    PropLogic.SOr (prop_for_exists_eq xs Gen, prop_for_comp (a1, a2, cmp, []))
+fun prop_for_comp (aa1, aa2, Eq, []) =
+    PropLogic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
+                    prop_for_comp (aa2, aa1, Leq, []))
+  | prop_for_comp (aa1, aa2, Leq, []) =
+    PropLogic.SOr (prop_for_annotation_atom_eq (aa1, Fls),
+                   prop_for_annotation_atom_eq (aa2, Gen))
+  | prop_for_comp (aa1, aa2, cmp, xs) =
+    PropLogic.SOr (prop_for_exists_eq xs Gen, prop_for_comp (aa1, aa2, cmp, []))
 
 fun fix_bool_options (NONE, NONE) = (false, false)
   | fix_bool_options (NONE, SOME b) = (b, b)
@@ -507,9 +507,9 @@
            | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
        (max_var downto 1) lits
 
-fun string_for_comp (a1, a2, cmp, xs) =
-  string_for_annotation_atom a1 ^ " " ^ string_for_comp_op cmp ^
-  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom a2
+fun string_for_comp (aa1, aa2, cmp, xs) =
+  string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^
+  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2
 
 fun print_problem lits comps sexps =
   trace_msg (fn () => "*** Problem:\n" ^
@@ -636,10 +636,10 @@
           accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
                 |> do_term body_t ||> apfst pop_bound
         val bound_M = mtype_of_mterm bound_m
-        val (M1, a, _) = dest_MFun bound_M
+        val (M1, aa, _) = dest_MFun bound_M
       in
         (MApp (MRaw (t0, MFun (bound_M, A Gen, bool_M)),
-               MAbs (abs_s, abs_T, M1, a,
+               MAbs (abs_s, abs_T, M1, aa,
                      MApp (MApp (MRaw (connective_t,
                                        mtype_for (fastype_of connective_t)),
                                  MApp (bound_m, MRaw (Bound 0, M1))),
@@ -769,9 +769,9 @@
               SOME t' =>
               let
                 val M = mtype_for T
-                val a = V (Unsynchronized.inc max_fresh)
+                val aa = V (Unsynchronized.inc max_fresh)
                 val (m', accum) = do_term t' (accum |>> push_bound T M)
-              in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
+              in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end
             | NONE =>
               ((case t' of
                   t1' $ Bound 0 =>
@@ -1049,15 +1049,15 @@
       tsp
     else
       let
-        fun should_finitize T a =
+        fun should_finitize T aa =
           case triple_lookup (type_match thy) finitizes T of
             SOME (SOME false) => false
-          | _ => resolve_annotation_atom lits a = A Fls
+          | _ => resolve_annotation_atom lits aa = A Fls
         fun type_from_mtype T M =
           case (M, T) of
             (MAlpha, _) => T
-          | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
-            Type (if should_finitize T a then @{type_name fin_fun}
+          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
+            Type (if should_finitize T aa then @{type_name fin_fun}
                   else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
           | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
             Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
@@ -1128,14 +1128,14 @@
                 | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
                                    [T1], [])
             in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
-          | MAbs (s, old_T, M, a, m') =>
+          | MAbs (s, old_T, M, aa, m') =>
             let
               val new_T = type_from_mtype old_T M
               val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
               val T' = fastype_of1 (new_T :: new_Ts, t')
             in
               Abs (s, new_T, t')
-              |> should_finitize (new_T --> T') a
+              |> should_finitize (new_T --> T') aa
                  ? construct_value ctxt stds (fin_fun_constr new_T T') o single
             end
       in