--- a/doc-src/Codegen/Thy/document/Adaptation.tex Tue Feb 21 12:10:47 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Tue Feb 21 13:19:16 2012 +0100
@@ -149,7 +149,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
+The \isa{HOL} \isa{Main} theory already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
theories of the \isa{HOL} library; beside being useful in
@@ -173,12 +173,12 @@
\isa{Suc} is eliminated; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}
and \isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}.
- \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}}}] provides an additional datatype
+ \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}] provides an additional datatype
\isa{index} which is mapped to target-language built-in
integers. Useful for code setups which involve e.g.~indexing
of target-language arrays. Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
- \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings. Useful
+ \item[\isa{String}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings. Useful
for code setups which involve e.g.~printing (error) messages.
Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Tue Feb 21 12:10:47 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Tue Feb 21 13:19:16 2012 +0100
@@ -372,7 +372,7 @@
arbitrary ML code as well.
A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} can be found in the
- \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.%
+ \isa{Predicate} theory.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Foundations.tex Tue Feb 21 12:10:47 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Tue Feb 21 13:19:16 2012 +0100
@@ -31,9 +31,9 @@
components which can be customised individually.
Conceptually all components operate on Isabelle's logic framework
- \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}. Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}
+ \isa{Pure}. Practically, the object logic \isa{HOL}
provides the necessary facilities to make use of the code generator,
- mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.
+ mainly since it is an extension of \isa{Pure}.
The constellation of the different components is visualized in the
following picture.
--- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Feb 21 12:10:47 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Feb 21 13:19:16 2012 +0100
@@ -30,7 +30,7 @@
\cite{scala-overview-tech-report}.
To profit from this tutorial, some familiarity and experience with
- \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
+ \isa{HOL} \cite{isa-tutorial} and its basic theories is assumed.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Feb 21 12:10:47 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Feb 21 13:19:16 2012 +0100
@@ -628,9 +628,9 @@
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving
- invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}}
+ invariants are available in the library, theory \isa{Mapping}
specifies key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping});
- these can be implemented by red-black-trees (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
+ these can be implemented by red-black-trees (theory \isa{RBT}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/HOL/Library/Dlist.thy Tue Feb 21 12:10:47 2012 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Feb 21 13:19:16 2012 +0100
@@ -182,7 +182,7 @@
subsection {* Quickcheck generators *}
-quickcheck_generator dlist constructors: empty, insert
+quickcheck_generator dlist predicate: distinct constructors: empty, insert
hide_const (open) member fold foldr empty insert remove map filter null member length fold
--- a/src/HOL/Library/RBT.thy Tue Feb 21 12:10:47 2012 +0100
+++ b/src/HOL/Library/RBT.thy Tue Feb 21 13:19:16 2012 +0100
@@ -171,6 +171,6 @@
subsection {* Quickcheck generators *}
-quickcheck_generator rbt constructors: empty, insert
+quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
end
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Feb 21 12:10:47 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Feb 21 13:19:16 2012 +0100
@@ -6,7 +6,7 @@
signature ABSTRACT_GENERATORS =
sig
- val quickcheck_generator : string -> term list -> theory -> theory
+ val quickcheck_generator : string -> term option -> term list -> theory -> theory
end;
structure Abstract_Generators : ABSTRACT_GENERATORS =
@@ -28,19 +28,20 @@
map check_type constrs
end
-fun gen_quickcheck_generator prep_tyco prep_term tyco_raw constrs_raw thy =
+fun gen_quickcheck_generator prep_tyco prep_term tyco_raw opt_pred_raw constrs_raw thy =
let
val ctxt = Proof_Context.init_global thy
val tyco = prep_tyco ctxt tyco_raw
+ val opt_pred = Option.map (prep_term ctxt) opt_pred_raw
val constrs = map (prep_term ctxt) constrs_raw
- val _ = check_constrs ctxt tyco constrs
+ val _ = check_constrs ctxt tyco constrs
val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
val name = Long_Name.base_name tyco
fun mk_dconstrs (Const (s, T)) =
(s, map (Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
| mk_dconstrs t = error (Syntax.string_of_term ctxt t ^
" is not a valid constructor for quickcheck_generator, which expects a constant.")
- fun the_descr thy _ =
+ fun the_descr _ _ =
let
val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
in
@@ -53,7 +54,9 @@
in
thy
|> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
+ |> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype)
|> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
+ |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
end
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
@@ -62,7 +65,10 @@
(fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
- Keyword.thy_decl (Parse.type_const -- (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
- >> (fn (tyco, constrs) => Toplevel.theory (quickcheck_generator_cmd tyco constrs)))
+ Keyword.thy_decl ((Parse.type_const --
+ Scan.option (Args.$$$ "predicate" |-- Parse.$$$ ":" |-- Parse.term)) --
+ (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
+ >> (fn ((tyco, opt_pred), constrs) =>
+ Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
end;
\ No newline at end of file
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Feb 21 12:10:47 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Feb 21 13:19:16 2012 +0100
@@ -23,6 +23,9 @@
val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
(string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ val instantiate_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+ (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+
end;
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Feb 21 12:10:47 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Feb 21 13:19:16 2012 +0100
@@ -14,6 +14,7 @@
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
+ val register_predicate : term * string -> Context.generic -> Context.generic
val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
type result = (bool * term list) option * Quickcheck.report option
@@ -96,9 +97,11 @@
val _ = Quickcheck.verbose_message ctxt
("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
val _ = current_size := k
- val ((result, report), timing) =
+ val ((result, report), time) =
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
- val _ = Quickcheck.add_timing timing current_result
+ val _ = if Config.get ctxt Quickcheck.timing then
+ Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
+ val _ = Quickcheck.add_timing time current_result
val _ = Quickcheck.add_report k report current_result
in
case result of
@@ -277,6 +280,37 @@
subst_bounds (map Free (rev vs'), body)
end
+
+structure Subtype_Predicates = Generic_Data
+(
+ type T = (term * string) list
+ val empty = []
+ val extend = I
+ val merge = AList.merge (op =) (K true)
+)
+
+val register_predicate = Subtype_Predicates.map o AList.update (op =)
+
+fun subtype_preprocess ctxt (T, (t, ts)) =
+ let
+ val preds = Subtype_Predicates.get (Context.Proof ctxt)
+ fun matches (p $ x) = AList.defined Term.could_unify preds p
+ fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
+ fun subst_of (tyco, v as Free (x, repT)) =
+ let
+ val [(info, _)] = Typedef.get_info ctxt tyco
+ val repT' = Logic.varifyT_global (#rep_type info)
+ val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
+ val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
+ in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
+ val (prems, concl) = strip_imp t
+ val subst = map subst_of (map_filter get_match prems)
+ val t' = Term.subst_free subst
+ (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
+ in
+ (T, (t', ts))
+ end
+
(* instantiation of type variables with concrete types *)
fun instantiate_goals lthy insts goals =
@@ -333,6 +367,7 @@
fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
let
+ val use_subtype = Config.get ctxt Quickcheck.use_subtype
fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
fun add_equation_eval_terms (t, eval_terms) =
case try HOLogic.dest_eq (snd (strip_imp t)) of
@@ -343,6 +378,7 @@
[(NONE, t)] => test_term generator ctxt catch_code_errors t
| ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
val goals' = instantiate_goals ctxt insts goals
+ |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
|> map (map (apsnd add_equation_eval_terms))
in
if Config.get ctxt Quickcheck.finite_types then
--- a/src/Pure/System/isabelle_process.ML Tue Feb 21 12:10:47 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML Tue Feb 21 13:19:16 2012 +0100
@@ -6,13 +6,13 @@
Startup phases:
. raw Posix process startup with uncontrolled output on stdout/stderr
- . stdout \002: ML running
+ . stderr \002: ML running
.. stdin/stdout/stderr freely available (raw ML loop)
.. protocol thread initialization
... rendezvous on system channel
... message INIT(pid): channels ready
- ... message STATUS(keywords)
- ... message READY: main loop ready
+ ... message RAW(keywords)
+ ... message RAW(ready): main loop ready
*)
signature ISABELLE_PROCESS =
@@ -165,7 +165,7 @@
fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
let
val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
- val _ = Output.physical_stdout Symbol.STX;
+ val _ = Output.physical_stderr Symbol.STX;
val _ = quick_and_dirty := true;
val _ = Goal.parallel_proofs := 0;
--- a/src/Pure/System/isabelle_process.scala Tue Feb 21 12:10:47 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala Tue Feb 21 13:19:16 2012 +0100
@@ -152,15 +152,15 @@
private val process_manager = Simple_Thread.fork("process_manager")
{
- val (startup_failed, startup_output) =
+ val (startup_failed, startup_errors) =
{
val expired = System.currentTimeMillis() + timeout.ms
val result = new StringBuilder(100)
var finished: Option[Boolean] = None
while (finished.isEmpty && System.currentTimeMillis() <= expired) {
- while (finished.isEmpty && process.stdout.ready) {
- val c = process.stdout.read
+ while (finished.isEmpty && process.stderr.ready) {
+ val c = process.stderr.read
if (c == 2) finished = Some(true)
else result += c.toChar
}
@@ -169,7 +169,7 @@
}
(finished.isEmpty || !finished.get, result.toString.trim)
}
- system_result(startup_output)
+ if (startup_errors != "") system_result(startup_errors)
if (startup_failed) {
put_result(Isabelle_Markup.EXIT, "Return code: 127")
--- a/src/Tools/jEdit/src/document_view.scala Tue Feb 21 12:10:47 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 21 13:19:16 2012 +0100
@@ -10,6 +10,7 @@
import isabelle._
+import scala.annotation.tailrec
import scala.collection.mutable
import scala.collection.immutable.SortedMap
import scala.actors.Actor._
@@ -354,11 +355,7 @@
private val WIDTH = 10
private val HEIGHT = 2
- private def line_to_y(line: Int): Int =
- (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
-
- private def y_to_line(y: Int): Int =
- (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
+ private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
setPreferredSize(new Dimension(WIDTH, 0))
@@ -366,7 +363,7 @@
addMouseListener(new MouseAdapter {
override def mousePressed(event: MouseEvent) {
- val line = y_to_line(event.getY)
+ val line = (event.getY * lines()) / getHeight
if (line >= 0 && line < text_area.getLineCount)
text_area.setCaretPosition(text_area.getLineStartOffset(line))
}
@@ -387,23 +384,44 @@
super.paintComponent(gfx)
Swing_Thread.assert()
- val buffer = model.buffer
- Isabelle.buffer_lock(buffer) {
- val snapshot = update_snapshot()
+ robust_body(()) {
+ val buffer = model.buffer
+ Isabelle.buffer_lock(buffer) {
+ val snapshot = update_snapshot()
+
+ gfx.setColor(getBackground)
+ gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+
+ val line_count = buffer.getLineCount
+ val char_count = buffer.getLength
+
+ val L = lines()
+ val H = getHeight()
- for {
- line <- 0 until buffer.getLineCount
- range <-
- try {
- Some(proper_line_range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line)))
+ @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
+ {
+ if (l < line_count && h < H) {
+ val p1 = p + H
+ val q1 = q + HEIGHT * L
+ val (l1, h1) =
+ if (p1 >= q1) (l + 1, h + (p1 - q) / L)
+ else (l + (q1 - p) / H, h + HEIGHT)
+
+ val start = buffer.getLineStartOffset(l)
+ val end =
+ if (l1 < line_count) buffer.getLineStartOffset(l1)
+ else char_count
+
+ Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
+ case None =>
+ case Some(color) =>
+ gfx.setColor(color)
+ gfx.fillRect(0, h, getWidth, h1 - h)
+ }
+ paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
}
- catch { case e: ArrayIndexOutOfBoundsException => None }
- color <- Isabelle_Rendering.overview_color(snapshot, range)
- } {
- val y = line_to_y(line)
- val h = (line_to_y(line + 1) - y) max 2
- gfx.setColor(color)
- gfx.fillRect(0, y, getWidth - 1, h)
+ }
+ paint_loop(0, 0, 0, 0)
}
}
}
--- a/src/Tools/quickcheck.ML Tue Feb 21 12:10:47 2012 +0100
+++ b/src/Tools/quickcheck.ML Tue Feb 21 13:19:16 2012 +0100
@@ -19,13 +19,14 @@
val depth : int Config.T
val no_assms : bool Config.T
val report : bool Config.T
+ val timeout : real Config.T
val timing : bool Config.T
val genuine_only : bool Config.T
val abort_potential : bool Config.T
val quiet : bool Config.T
val verbose : bool Config.T
- val timeout : real Config.T
- val allow_function_inversion : bool Config.T;
+ val use_subtype : bool Config.T
+ val allow_function_inversion : bool Config.T
val finite_types : bool Config.T
val finite_type_size : int Config.T
val set_active_testers: string list -> Context.generic -> Context.generic
@@ -177,11 +178,16 @@
val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+
val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
+
val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
-val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+
+val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
+
val allow_function_inversion =
Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
@@ -438,6 +444,7 @@
| parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
| parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
| parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
+ | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))
| parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
| parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
| parse_test_param ("allow_function_inversion", [arg]) =