summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Mon, 07 Dec 2009 13:40:45 +0100 | |

changeset 34038 | a2736debeabd |

parent 34019 | 549855d22044 |

child 34039 | 1fba360b5443 |

make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes

doc-src/Nitpick/nitpick.tex | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/Nitpick/nitpick.ML | file | annotate | diff | comparison | revisions |

--- 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 ();