merged;
authorwenzelm
Wed, 20 Apr 2011 17:17:01 +0200
changeset 42438 cf963c834435
parent 42437 4344b3654961 (diff)
parent 42429 7691cc61720a (current diff)
child 42439 9efdd0af15ac
merged;
src/HOL/Mutabelle/mutabelle_extra.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Mercurial/isabelle-style-1.3.1.diff	Wed Apr 20 17:17:01 2011 +0200
@@ -0,0 +1,140 @@
+diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
+--- gitweb/changelogentry.tmpl	2011-04-20 12:13:37.000000000 +0200
++++ isabelle/changelogentry.tmpl	2011-04-20 12:13:37.000000000 +0200
+@@ -1,14 +1,12 @@
+ <div>
+-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age} ago</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+-</div>
+-<div class="title_text">
+-<div class="log_link">
+-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
+-</div>
+-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
++<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
++{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+ </div>
+ <div class="log_body">
+ {desc|strip|escape|addbreaks|nonempty}
+ <br/>
++<div class="files">
++{files}
++</div>
+ <br/>
+ </div>
+diff -Naur gitweb/changeset.tmpl isabelle/changeset.tmpl
+--- gitweb/changeset.tmpl	2011-04-20 12:13:37.000000000 +0200
++++ isabelle/changeset.tmpl	2011-04-20 12:13:37.000000000 +0200
+@@ -29,7 +29,7 @@
+ <div class="title_text">
+ <table cellspacing="0">
+ <tr><td>author</td><td>{author|obfuscate}</td></tr>
+-<tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
++<tr><td></td><td>{date|date} ({date|age})</td></tr>
+ {branch%changesetbranch}
+ <tr><td>changeset {rev}</td><td style="font-family:monospace">{node|short}</td></tr>
+ {parent%changesetparent}
+diff -Naur gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
+--- gitweb/fileannotate.tmpl	2011-04-20 12:13:37.000000000 +0200
++++ isabelle/fileannotate.tmpl	2011-04-20 12:13:37.000000000 +0200
+@@ -36,7 +36,7 @@
+  <td>{author|obfuscate}</td></tr>
+ <tr>
+  <td></td>
+- <td>{date|date} ({date|age} ago)</td></tr>
++ <td>{date|date} ({date|age})</td></tr>
+ {branch%filerevbranch}
+ <tr>
+  <td>changeset {rev}</td>
+diff -Naur gitweb/filerevision.tmpl isabelle/filerevision.tmpl
+--- gitweb/filerevision.tmpl	2011-04-20 12:13:37.000000000 +0200
++++ isabelle/filerevision.tmpl	2011-04-20 12:13:37.000000000 +0200
+@@ -36,7 +36,7 @@
+  <td>{author|obfuscate}</td></tr>
+ <tr>
+  <td></td>
+- <td>{date|date} ({date|age} ago)</td></tr>
++ <td>{date|date} ({date|age})</td></tr>
+ {branch%filerevbranch}
+ <tr>
+  <td>changeset {rev}</td>
+diff -Naur gitweb/graph.tmpl isabelle/graph.tmpl
+--- gitweb/graph.tmpl	2011-04-20 12:13:37.000000000 +0200
++++ isabelle/graph.tmpl	2011-04-20 12:13:37.000000000 +0200
+@@ -63,7 +63,7 @@
+ var revlink = '<li style="_STYLE"><span class="desc">';
+ revlink += '<a class="list" href="{url}rev/_NODEID{sessionvars%urlparameter}" title="_NODEID"><b>_DESC</b></a>';
+ revlink += '</span> _TAGS';
+-revlink += '<span class="info">_DATE ago, by _USER</span></li>';
++revlink += '<span class="info">_DATE, by _USER</span></li>';
+ 
+ graph.vertex = function(x, y, color, parity, cur) {
+ 	
+diff -Naur gitweb/map isabelle/map
+--- gitweb/map	2011-04-20 12:13:37.000000000 +0200
++++ isabelle/map	2011-04-20 12:13:37.000000000 +0200
+@@ -78,7 +78,7 @@
+   <tr style="font-family:monospace" class="parity{parity}">
+     <td class="linenr" style="text-align: right;">
+       <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
+-         title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
++         title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
+     </td>
+     <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
+     <td><pre>{line|escape}</pre></td>
+@@ -150,7 +150,7 @@
+ tags = tags.tmpl
+ tagentry = '
+   <tr class="parity{parity}">
+-    <td class="age"><i>{date|age} ago</i></td>
++    <td class="age"><i>{date|age}</i></td>
+     <td><a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}"><b>{tag|escape}</b></a></td>
+     <td class="link">
+       <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a> |
+@@ -161,7 +161,7 @@
+ branches = branches.tmpl
+ branchentry = '
+   <tr class="parity{parity}">
+-    <td class="age"><i>{date|age} ago</i></td>
++    <td class="age"><i>{date|age}</i></td>
+     <td><a class="list" href="{url}shortlog/{node|short}{sessionvars%urlparameter}"><b>{node|short}</b></a></td>
+     <td class="{status}">{branch|escape}</td>
+     <td class="link">
+@@ -204,11 +204,12 @@
+ inbranchtag = '<span class="inbranchtag" title="{name}">{name}</span> '
+ shortlogentry = '
+   <tr class="parity{parity}">
+-    <td class="age"><i>{date|age} ago</i></td>
++    <td class="age"><i>{date|age}</i></td>
+     <td><i>{author|person}</i></td>
++    <td><i>{date|shortdate}</i></td>
+     <td>
+       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+-        <b>{desc|strip|firstline|escape|nonempty}</b>
++        <b>{desc|strip|escape|nonempty}</b>
+         <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
+       </a>
+     </td>
+@@ -219,10 +220,12 @@
+   </tr>'
+ filelogentry = '
+   <tr class="parity{parity}">
+-    <td class="age"><i>{date|age} ago</i></td>
++    <td class="age"><i>{date|age}</i></td>
++    <td><i>{author|person}</i></td>
++    <td><i>{date|shortdate}</i></td>
+     <td>
+       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+-        <b>{desc|strip|firstline|escape|nonempty}</b>
++        <b>{desc|strip|escape|nonempty}</b>
+       </a>
+     </td>
+     <td class="link">
+@@ -238,7 +241,7 @@
+     </td>
+     <td>{description}</td>
+     <td>{contact|obfuscate}</td>
+-    <td class="age">{lastchange|age} ago</td>
++    <td class="age">{lastchange|age}</td>
+     <td class="indexlinks">{archives%indexarchiveentry}</td>
+     <td><div class="rss_logo"><a href="{url}rss-log">RSS</a> <a href="{url}atom-log">Atom</a></div></td>
+   </tr>\n'
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Mercurial/isabelle-style-1.4.3--1.8.2.diff	Wed Apr 20 17:17:01 2011 +0200
@@ -0,0 +1,60 @@
+diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
+--- gitweb/changelogentry.tmpl	2011-04-20 12:27:29.000000000 +0200
++++ isabelle/changelogentry.tmpl	2011-04-20 12:32:48.000000000 +0200
+@@ -1,14 +1,12 @@
+ <div>
+-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+-</div>
+-<div class="title_text">
+-<div class="log_link">
+-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
+-</div>
+-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
++<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
++{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+ </div>
+ <div class="log_body">
+ {desc|strip|escape|addbreaks|nonempty}
+ <br/>
++<div class="files">
++{files}
++</div>
+ <br/>
+ </div>
+diff -Naur gitweb/map isabelle/map
+--- gitweb/map	2011-04-20 12:27:29.000000000 +0200
++++ isabelle/map	2011-04-20 12:32:48.000000000 +0200
+@@ -78,7 +78,7 @@
+   <tr style="font-family:monospace" class="parity{parity}">
+     <td class="linenr" style="text-align: right;">
+       <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
+-         title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
++         title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
+     </td>
+     <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
+     <td><pre>{line|escape}</pre></td>
+@@ -206,9 +206,10 @@
+   <tr class="parity{parity}">
+     <td class="age"><i>{date|age}</i></td>
+     <td><i>{author|person}</i></td>
++    <td><i>{date|shortdate}</i></td>
+     <td>
+       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+-        <b>{desc|strip|firstline|escape|nonempty}</b>
++        <b>{desc|strip|escape|nonempty}</b>
+         <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
+       </a>
+     </td>
+@@ -220,9 +221,11 @@
+ filelogentry = '
+   <tr class="parity{parity}">
+     <td class="age"><i>{date|age}</i></td>
++    <td><i>{author|person}</i></td>
++    <td><i>{date|shortdate}</i></td>
+     <td>
+       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+-        <b>{desc|strip|firstline|escape|nonempty}</b>
++        <b>{desc|strip|escape|nonempty}</b>
+       </a>
+     </td>
+     <td class="link">
--- a/Admin/Mercurial/isabelle-style.diff	Wed Apr 20 16:49:52 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-diff -r gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
-2,8c2,3
-< <a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age} ago</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-< </div>
-< <div class="title_text">
-< <div class="log_link">
-< <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
-< </div>
-< <i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
----
-> <a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
-> {author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-12a8,10
-> <div class="files">
-> {files}
-> </div>
-diff -r gitweb/changeset.tmpl isabelle/changeset.tmpl
-32c32
-< <tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
----
-> <tr><td></td><td>{date|date} ({date|age})</td></tr>
-diff -r gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
-39c39
-<  <td>{date|date} ({date|age} ago)</td></tr>
----
->  <td>{date|date} ({date|age})</td></tr>
-diff -r gitweb/filerevision.tmpl isabelle/filerevision.tmpl
-39c39
-<  <td>{date|date} ({date|age} ago)</td></tr>
----
->  <td>{date|date} ({date|age})</td></tr>
-diff -r gitweb/graph.tmpl isabelle/graph.tmpl
-66c66
-< revlink += '<span class="info">_DATE ago, by _USER</span></li>';
----
-> revlink += '<span class="info">_DATE, by _USER</span></li>';
-diff -r gitweb/map isabelle/map
-81c81
-<          title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
----
->          title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
-153c153
-<     <td class="age"><i>{date|age} ago</i></td>
----
->     <td class="age"><i>{date|age}</i></td>
-164c164
-<     <td class="age"><i>{date|age} ago</i></td>
----
->     <td class="age"><i>{date|age}</i></td>
-207c207
-<     <td class="age"><i>{date|age} ago</i></td>
----
->     <td class="age"><i>{date|age}</i></td>
-208a209
->     <td><i>{date|shortdate}</i></td>
-211c212
-<         <b>{desc|strip|firstline|escape|nonempty}</b>
----
->         <b>{desc|strip|escape|nonempty}</b>
-222c223,225
-<     <td class="age"><i>{date|age} ago</i></td>
----
->     <td class="age"><i>{date|age}</i></td>
->     <td><i>{author|person}</i></td>
->     <td><i>{date|shortdate}</i></td>
-225c228
-<         <b>{desc|strip|firstline|escape|nonempty}</b>
----
->         <b>{desc|strip|escape|nonempty}</b>
-241c244
-<     <td class="age">{lastchange|age} ago</td>
----
->     <td class="age">{lastchange|age}</td>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 16:49:52 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 17:17:01 2011 +0200
@@ -273,7 +273,9 @@
  @{const_name "ord_fun_inst.less_fun"},
  @{const_name Metis.fequal},
  @{const_name Meson.skolem},
- @{const_name transfer_morphism}
+ @{const_name transfer_morphism},
+ @{const_name enum_prod_inst.enum_all_prod},
+ @{const_name enum_prod_inst.enum_ex_prod}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Apr 20 16:49:52 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Apr 20 17:17:01 2011 +0200
@@ -116,7 +116,14 @@
     KK.TupleIndex (length js,
                    fold (fn j => fn accum => accum * univ_card + j) js 0)
 
-val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq
+(* This code is not just a silly optimization: It works around a limitation in
+   Kodkodi, whereby {} (i.e., KK.TupleProduct) is always given the cardinality
+   of the bound in which it appears, resulting in Kodkod arity errors. *)
+fun tuple_product (ts as KK.TupleSet []) _ = ts
+  | tuple_product _ (ts as KK.TupleSet []) = ts
+  | tuple_product ts1 ts2 = KK.TupleProduct (ts1, ts2)
+
+val tuple_set_from_atom_schema = fold1 tuple_product o map KK.TupleAtomSeq
 val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
 
 val single_atom = KK.TupleSet o single o KK.Tuple o single
@@ -358,17 +365,17 @@
          fun tuple_perhaps_needy_atom upper j =
            single_atom j
            |> not discr
-              ? (fn ts => KK.TupleProduct (ts,
-                              case exact_bound_for_perhaps_needy_atom j of
-                                SOME ts => ts
-                              | NONE => if upper then upper_bound_for_rep R2
-                                        else KK.TupleSet []))
+              ? (fn ts => tuple_product ts
+                              (case exact_bound_for_perhaps_needy_atom j of
+                                 SOME ts => ts
+                               | NONE => if upper then upper_bound_for_rep R2
+                                         else KK.TupleSet []))
          fun bound_tuples upper =
            if null T1_need_vals then
              if upper then
                KK.TupleAtomSeq (epsilon - delta, delta + j0)
                |> not discr
-                  ? (fn ts => KK.TupleProduct (ts, upper_bound_for_rep R2))
+                  ? (fn ts => tuple_product ts (upper_bound_for_rep R2))
              else
                KK.TupleSet []
            else
@@ -393,9 +400,8 @@
               if T1 = T2 andalso epsilon > delta andalso
                  is_datatype_acyclic dtype then
                 index_seq delta (epsilon - delta)
-                |> map (fn j =>
-                           KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
-                               KK.TupleAtomSeq (atom_seq_for_self_rec j)))
+                |> map (fn j => tuple_product (KK.TupleSet [KK.Tuple [j + j0]])
+                                    (KK.TupleAtomSeq (atom_seq_for_self_rec j)))
                 |> n_fold_tuple_union
               else
                 bound_tuples true]
--- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Apr 20 16:49:52 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Apr 20 17:17:01 2011 +0200
@@ -294,4 +294,28 @@
 quickcheck[random, size = 10]
 oops
 
+subsection {* Examples with locales *}
+
+locale Truth
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[expect = no_counterexample]
+oops
+
 end
+
+interpretation Truth .
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[expect = counterexample]
+oops
+
+end
+
+end
--- a/src/Tools/quickcheck.ML	Wed Apr 20 16:49:52 2011 +0200
+++ b/src/Tools/quickcheck.ML	Wed Apr 20 17:17:01 2011 +0200
@@ -507,10 +507,14 @@
     maps (fn (label, time) =>
       Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
 
-fun pretty_counterex_and_reports ctxt auto (result :: _) =
-  Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
-    (* map (pretty_reports ctxt) (reports_of result) :: *)
-    (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
+fun pretty_counterex_and_reports ctxt auto [] =
+    Pretty.chunks [Pretty.strs (tool_name auto ::
+        space_explode " " "is used in a locale where no interpretation is provided."),
+      Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
+  | pretty_counterex_and_reports ctxt auto (result :: _) =
+    Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
+      (* map (pretty_reports ctxt) (reports_of result) :: *)
+      (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
 
 (* automatic testing *)
 
@@ -593,11 +597,11 @@
 fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
 
 fun check_expectation state results =
-  (if found_counterexample (hd results) andalso expect (Proof.context_of state) = No_Counterexample
+  (if exists found_counterexample results andalso expect (Proof.context_of state) = No_Counterexample
   then
     error ("quickcheck expected to find no counterexample but found one")
   else
-    (if not (found_counterexample (hd results)) andalso expect (Proof.context_of state) = Counterexample
+    (if not (exists found_counterexample results) andalso expect (Proof.context_of state) = Counterexample
     then
       error ("quickcheck expected to find a counterexample but did not find one")
     else ()))