make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
--- a/doc-src/Nitpick/nitpick.tex Mon Dec 07 12:21:15 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex Mon Dec 07 13:40:45 2009 +0100
@@ -1517,15 +1517,13 @@
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
-Hint: Maybe you forgot a type constraint?
\postw
-It's hard to see why this is a counterexample. The hint is of no help here. To
-improve readability, we will restrict the theorem to \textit{nat}, so that we
-don't need to look up the value of the $\textit{op}~{<}$ constant to find out
-which element is smaller than the other. In addition, we will tell Nitpick to
-display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
-gives
+It's hard to see why this is a counterexample. To improve readability, we will
+restrict the theorem to \textit{nat}, so that we don't need to look up the value
+of the $\textit{op}~{<}$ constant to find out which element is smaller than the
+other. In addition, we will tell Nitpick to display the value of
+$\textit{insort}~t~x$ using the \textit{eval} option. This gives
\prew
\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 07 12:21:15 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 07 13:40:45 2009 +0100
@@ -164,17 +164,15 @@
(* ('a * bool option) list -> bool *)
fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
-val weaselly_sorts =
- [@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus},
- @{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn},
- @{sort ord}, @{sort eq}, @{sort number}]
-(* theory -> typ -> bool *)
-fun is_tfree_with_weaselly_sort thy (TFree (_, S)) =
- exists (curry (Sign.subsort thy) S) weaselly_sorts
- | is_tfree_with_weaselly_sort _ _ = false
-(* theory term -> bool *)
-val has_weaselly_sorts =
- exists_type o exists_subtype o is_tfree_with_weaselly_sort
+val syntactic_sorts =
+ @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+ @{sort number}
+(* typ -> bool *)
+fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
+ subset (op =) (S, syntactic_sorts)
+ | has_tfree_syntactic_sort _ = false
+(* term -> bool *)
+val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
(* (unit -> string) -> Pretty.T *)
fun plazy f = Pretty.blk (0, pstrs (f ()))
@@ -575,7 +573,7 @@
| NONE => print "No confirmation by \"auto\".")
else
();
- if has_weaselly_sorts thy orig_t then
+ if has_syntactic_sorts orig_t then
print "Hint: Maybe you forgot a type constraint?"
else
();