simplified context and data management -- plain ctxt: Proof.context is default for most operations;

--- a/src/HOL/Spec_Check/Spec_Check.thy	Thu May 30 20:57:55 2013 +0200
+++ b/src/HOL/Spec_Check/Spec_Check.thy	Thu May 30 21:28:54 2013 +0200
@@ -9,7 +9,6 @@
 ML_file "gen_construction.ML"
 ML_file "spec_check.ML"
 ML_file "output_style.ML"
-
-setup {* Perl_Style.setup #> CMStyle.setup *}
+setup Output_Style.setup
 
 end
\ No newline at end of file

--- a/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 20:57:55 2013 +0200
+++ b/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 21:28:54 2013 +0200
@@ -9,8 +9,8 @@
 sig
   val register : string * (string * string) -> theory -> theory
   type mltype
-  val parse_pred : string -> string * mltype;
-  val build_check : theory -> string -> mltype * string -> string
+  val parse_pred : string -> string * mltype
+  val build_check : Proof.context -> string -> mltype * string -> string
   (*val safe_check : string -> mltype * string -> string*)
   val string_of_bool : bool -> string
   val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
@@ -111,8 +111,8 @@
   fun merge data : T = Symtab.merge (K true) data
 )
 
-fun data_of thy tycon =
-  (case Symtab.lookup (Data.get thy) tycon of
+fun data_of ctxt tycon =
+  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
     SOME data => data
   | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
 
@@ -129,44 +129,50 @@
   | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
 
 fun compose_generator _ Var = "Generator.int"
-  | compose_generator thy (Con (s, types)) =
-      combine (generator_of thy s) (map (compose_generator thy) types)
-  | compose_generator thy (Tuple t) =
-    let
-      fun tuple_body t = space_implode ""
-        (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
-        compose_generator thy ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
-      fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-    in "fn r0 => let " ^ tuple_body t ^
-      "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" end;
+  | compose_generator ctxt (Con (s, types)) =
+      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
+  | compose_generator ctxt (Tuple t) =
+      let
+        fun tuple_body t = space_implode ""
+          (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
+          compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
+        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+      in
+        "fn r0 => let " ^ tuple_body t ^
+        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
+      end;
 
 fun compose_printer _ Var = "Int.toString"
-  | compose_printer thy (Con (s, types)) =
-      combine (printer_of thy s) (map (compose_printer thy) types)
-  | compose_printer thy (Tuple t) =
-    let
-      fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-      fun tuple_body t = space_implode " ^ \", \" ^ "
-        (map (fn (ty, n) => "(" ^ compose_printer thy ty ^ ") x" ^ string_of_int n)
-        (t ~~ (1 upto (length t))))
-    in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
+  | compose_printer ctxt (Con (s, types)) =
+      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
+  | compose_printer ctxt (Tuple t) =
+      let
+        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+        fun tuple_body t = space_implode " ^ \", \" ^ "
+          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
+          (t ~~ (1 upto (length t))))
+      in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
 
 (*produce compilable string*)
-fun build_check thy name (ty, spec) = "Spec_Check.checkGen (ML_Context.the_generic_context ()) ("
-  ^ compose_generator thy ty ^ ", SOME (" ^ compose_printer thy ty ^ ")) (\""
+fun build_check ctxt name (ty, spec) =
+  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
+  ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
   ^ name ^ "\", Property.pred (" ^ spec ^ "));";
 
 (*produce compilable string - non-eqtype functions*)
 (*
 fun safe_check name (ty, spec) =
   let
-    val default = case AList.lookup (op =) (!gen_table) "->"
-      of NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
-      | SOME entry => entry
-  in (gen_table := AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\""))
-   (!gen_table);
+    val default =
+      (case AList.lookup (op =) (!gen_table) "->" of
+        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
+      | SOME entry => entry)
+  in
+   (gen_table :=
+     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
     build_check name (ty, spec) before
-    gen_table := AList.update (op =) ("->", default) (!gen_table)) end;
+    gen_table := AList.update (op =) ("->", default) (!gen_table))
+  end;
 *)
 
 end;

--- a/src/HOL/Spec_Check/generator.ML	Thu May 30 20:57:55 2013 +0200
+++ b/src/HOL/Spec_Check/generator.ML	Thu May 30 21:28:54 2013 +0200
@@ -74,12 +74,12 @@
 val string = vector CharVector.tabulate
 
 fun substring gen r =
-    let val (s, r') = gen r
-        val (i, r'') = range (0, String.size s) r'
-        val (j, r''') = range (0, String.size s - i) r''
-    in
-      (Substring.substring (s, i, j), r''')
-    end
+  let val (s, r') = gen r
+      val (i, r'') = range (0, String.size s) r'
+      val (j, r''') = range (0, String.size s - i) r''
+  in
+    (Substring.substring (s, i, j), r''')
+  end
 
 fun cochar c =
   if Char.ord c = 0 then variant 0
@@ -179,8 +179,12 @@
         val _ =  seed := new_seed
         val _ = table := AList.update (op =) (k, new_val) (!table)
       in new_val end
-  in (fn v1 => case AList.lookup (op =) (!table) v1 of
-    NONE => new_entry v1 | SOME v2 => v2, r') end;
+  in
+    (fn v1 =>
+      case AList.lookup (op =) (!table) v1 of
+        NONE => new_entry v1
+      | SOME v2 => v2, r')
+  end;
 
 (* unit *)
 

--- a/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:57:55 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 21:28:54 2013 +0200
@@ -5,20 +5,27 @@
 Output styles for presenting Spec_Check's results.
 *)
 
-structure Perl_Style =
+signature OUTPUT_STYLE =
+sig
+  val setup: theory -> theory
+end
+
+structure Output_Style: OUTPUT_STYLE =
 struct
 
+(* perl style *)
+
 local
 
 open StringCvt
 
-fun new context tag =
+fun new ctxt tag =
   let
-    val target = Config.get_generic context Spec_Check.gen_target
-    val namew = Config.get_generic context Spec_Check.column_width
-    val sort_examples = Config.get_generic context Spec_Check.sort_examples
-    val show_stats = Config.get_generic context Spec_Check.show_stats
-    val limit = Config.get_generic context Spec_Check.examples
+    val target = Config.get ctxt Spec_Check.gen_target
+    val namew = Config.get ctxt Spec_Check.column_width
+    val sort_examples = Config.get ctxt Spec_Check.sort_examples
+    val show_stats = Config.get ctxt Spec_Check.show_stats
+    val limit = Config.get ctxt Spec_Check.examples
 
     val resultw = 8
     val countw = 20
@@ -73,27 +80,23 @@
       if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
       else (writeln (update (stats, badobjs) true); err badobjs)
   in
-    {status=status, finish=finish}
+    {status = status, finish = finish}
   end
 
 in
-  val setup = Spec_Check.register_style ("Perl", new)
-end
-
+  val perl_style = Spec_Check.register_style ("Perl", new)
 end
 
+
 (* CM style: meshes with CM output; highlighted in sml-mode *)
 
-structure CMStyle =
-struct
-
 local
 
 fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
 
-fun new context tag =
+fun new ctxt tag =
   let
-    val gen_target = Config.get_generic context Spec_Check.gen_target
+    val gen_target = Config.get ctxt Spec_Check.gen_target
     val _ = writeln ("[testing " ^ tag ^ "... ")
     fun finish ({count, ...}, badobjs) =
       (case (count, badobjs) of
@@ -114,7 +117,12 @@
   end
 
 in
-  val setup = Spec_Check.register_style ("CM", new)
+  val cm_style = Spec_Check.register_style ("CM", new)
 end
 
+
+(* setup *)
+
+val setup = perl_style #> cm_style
+
 end

--- a/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:57:55 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 21:28:54 2013 +0200
@@ -15,13 +15,13 @@
   val column_width : int Config.T
   val style : string Config.T
 
-  type output_style = Context.generic -> string ->
+  type output_style = Proof.context -> string ->
     {status : string option * Property.result * (Property.stats  * string option list) -> unit,
      finish: Property.stats * string option list -> unit}
 
   val register_style : (string * output_style) -> theory -> theory
 
-  val checkGen : Context.generic ->
+  val checkGen : Proof.context ->
     'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
 
   val check_property : Proof.context -> string -> unit
@@ -46,11 +46,11 @@
 type ('a, 'b) reader = 'b -> ('a * 'b) option
 type 'a rep = ('a -> string) option
 
-type output_style = Context.generic -> string ->
+type output_style = Proof.context -> string ->
   {status: string option * Property.result * (Property.stats * string option list) -> unit,
    finish: Property.stats * string option list -> unit}
 
-fun limit context gen = Generator.limit (Config.get_generic context gen_max) gen
+fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
 
 structure Style = Theory_Data
 (
@@ -60,11 +60,11 @@
   fun merge data : T = Symtab.merge (K true) data
 )
 
-fun get_style context =
-  let val name = Config.get_generic context style
-  in case Symtab.lookup (Style.get (Context.theory_of context)) name of
-      SOME style => style context
-    | NONE => error ("No style called " ^ quote name ^ " found")
+fun get_style ctxt =
+  let val name = Config.get ctxt style in
+    (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
+      SOME style => style ctxt
+    | NONE => error ("No style called " ^ quote name ^ " found"))
   end
 
 fun register_style (name, style) = Style.map (Symtab.update (name, style))
@@ -72,11 +72,11 @@
 
 (* testing functions *)
 
-fun cpsCheck context s0 shrink (next, show) (tag, prop) =
+fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
   let
     val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
 
-    val {status, finish} = get_style context tag
+    val {status, finish} = get_style ctxt tag
     fun status' (obj, result, (stats, badobjs)) =
       let
         val badobjs' = if Property.failure result then obj :: badobjs else badobjs
@@ -96,7 +96,7 @@
 
     fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
       | iter (SOME (obj, stream), (stats, badobjs)) =
-        if #count stats >= Config.get_generic context gen_target then
+        if #count stats >= Config.get ctxt gen_target then
           finish (stats, map apply_show badobjs)
         else
           let
@@ -110,19 +110,20 @@
     fn stream => iter (next stream, (s0, []))
   end
 
-fun check' context s0 = cpsCheck context s0 (fn _ => [])
-fun check context = check' context Property.stats
-fun checks context = cpsCheck context Property.stats
-
-fun checkGen context (gen, show) (tag, prop) =
-  check' context {count=0, tags=[("__GEN", 0)]} (limit context gen, show) (tag, prop) Generator.stream
+fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
+fun check ctxt = check' ctxt Property.stats
+fun checks ctxt = cpsCheck ctxt Property.stats
 
-fun checkGenShrink context shrink (gen, show) (tag, prop) =
-  cpsCheck context {count=0, tags=[("__GEN", 0)]} shrink
-    (limit context gen, show) (tag, prop) Generator.stream
+fun checkGen ctxt (gen, show) (tag, prop) =
+  check' ctxt {count = 0, tags = [("__GEN", 0)]}
+    (limit ctxt gen, show) (tag, prop) Generator.stream
 
-fun checkOne context show (tag, prop) obj =
-  check context (List.getItem, show) (tag, prop) [obj]
+fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
+  cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
+    (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkOne ctxt show (tag, prop) obj =
+  check ctxt (List.getItem, show) (tag, prop) [obj]
 
 (*call the compiler and pass resulting type string to the parser*)
 fun determine_type ctxt s =
@@ -156,7 +157,8 @@
     fun dot c = c = #"."
     fun space c = c = #" "
     val (head, code) = Substring.splitl (not o dot) (Substring.full s)
-  in (String.tokens space (Substring.string head),
+  in
+   (String.tokens space (Substring.string head),
     Substring.string (Substring.dropl dot code))
   end;
 
@@ -176,7 +178,7 @@
   let
     val func = make_fun s
     val (_, ty) = determine_type ctxt func
-  in run_test ctxt (check (Proof_Context.theory_of ctxt) "Check" (ty, func)) end;
+  in run_test ctxt (check ctxt "Check" (ty, func)) end;
 
 val check_property = gen_check_property Gen_Construction.build_check
 (*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
@@ -185,7 +187,7 @@
 fun gen_check_property_f check ctxt s =
   let
     val (name, ty) = determine_type ctxt s
-  in run_test ctxt (check (Proof_Context.theory_of ctxt) name (ty, s)) end;
+  in run_test ctxt (check ctxt name (ty, s)) end;
 
 val check_property_f = gen_check_property_f Gen_Construction.build_check
 (*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)