# HG changeset patch
# User wenzelm
# Date 1369940275 -7200
# Node ID afca6a99a361c04bb3a5c2ebd6474b358cbea8e1
# Parent  81fcc11d8c658cf0c1dc222d68f8156c9ec101c4
more conventional spelling and grammar;

diff -r 81fcc11d8c65 -r afca6a99a361 src/HOL/Spec_Check/gen_construction.ML
--- a/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 20:38:50 2013 +0200
+++ b/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 20:57:55 2013 +0200
@@ -68,7 +68,7 @@
 and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
   >> (fn (t, tl) => Tuple (t :: tl))) s;
 
-(*Parses entire type + name*)
+(*Parse entire type + name*)
 fun parse_function s =
   let
     val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
@@ -77,7 +77,7 @@
     val (typ, _) = Scan.finite stop parse_type ty
   in (name, typ) end;
 
-(*Creates desired output*)
+(*Create desired output*)
 fun parse_pred s =
   let
     val (name, Con ("->", t :: _)) = parse_function s
@@ -111,8 +111,10 @@
   fun merge data : T = Symtab.merge (K true) data
 )
 
-fun data_of thy tycon = case Symtab.lookup (Data.get thy) tycon of SOME data => data
-  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)
+fun data_of thy tycon =
+  (case Symtab.lookup (Data.get thy) tycon of
+    SOME data => data
+  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
 
 val generator_of = fst oo data_of
 val printer_of = snd oo data_of
@@ -149,12 +151,12 @@
         (t ~~ (1 upto (length t))))
     in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
 
-(*produces compilable string*)
+(*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 ^ ")) (\""
   ^ name ^ "\", Property.pred (" ^ spec ^ "));";
 
-(*produces compilable string - non-eqtype functions*)
+(*produce compilable string - non-eqtype functions*)
 (*
 fun safe_check name (ty, spec) =
   let
diff -r 81fcc11d8c65 -r afca6a99a361 src/HOL/Spec_Check/output_style.ML
--- a/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:38:50 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:57:55 2013 +0200
@@ -12,13 +12,13 @@
 
 open StringCvt
 
-fun new ctxt tag =
+fun new context tag =
   let
-    val target = Config.get_generic ctxt Spec_Check.gen_target
-    val namew = Config.get_generic ctxt Spec_Check.column_width
-    val sort_examples = Config.get_generic ctxt Spec_Check.sort_examples
-    val show_stats = Config.get_generic ctxt Spec_Check.show_stats
-    val limit = Config.get_generic ctxt Spec_Check.examples
+    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 resultw = 8
     val countw = 20
@@ -91,9 +91,9 @@
 
 fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
 
-fun new ctxt tag =
+fun new context tag =
   let
-    val gen_target = Config.get_generic ctxt Spec_Check.gen_target
+    val gen_target = Config.get_generic context Spec_Check.gen_target
     val _ = writeln ("[testing " ^ tag ^ "... ")
     fun finish ({count, ...}, badobjs) =
       (case (count, badobjs) of
@@ -102,13 +102,13 @@
             if n >= gen_target then "ok]"
             else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
       | (_, es) =>
-        let
-          val wd = size (string_of_int (length es))
-          fun each (NONE, _) = ()
-            | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
-         in
-           (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
-         end)
+          let
+            val wd = size (string_of_int (length es))
+            fun each (NONE, _) = ()
+              | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+          in
+            (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+          end)
   in
     {status = K (), finish = finish}
   end
diff -r 81fcc11d8c65 -r afca6a99a361 src/HOL/Spec_Check/spec_check.ML
--- a/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:38:50 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:57:55 2013 +0200
@@ -50,7 +50,7 @@
   {status: string option * Property.result * (Property.stats * string option list) -> unit,
    finish: Property.stats * string option list -> unit}
 
-fun limit ctxt gen = Generator.limit (Config.get_generic ctxt gen_max) gen
+fun limit context gen = Generator.limit (Config.get_generic context gen_max) gen
 
 structure Style = Theory_Data
 (
@@ -60,22 +60,23 @@
   fun merge data : T = Symtab.merge (K true) data
 )
 
-fun get_style ctxt =
-  let val name = Config.get_generic ctxt style
-  in case Symtab.lookup (Style.get (Context.theory_of ctxt)) name of
-      SOME style => style ctxt
+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")
   end
 
 fun register_style (name, style) = Style.map (Symtab.update (name, style))
 
+
 (* testing functions *)
 
-fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
+fun cpsCheck context 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 ctxt tag
+    val {status, finish} = get_style context tag
     fun status' (obj, result, (stats, badobjs)) =
       let
         val badobjs' = if Property.failure result then obj :: badobjs else badobjs
@@ -95,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 ctxt gen_target then
+        if #count stats >= Config.get_generic context gen_target then
           finish (stats, map apply_show badobjs)
         else
           let
@@ -109,44 +110,44 @@
     fn stream => iter (next stream, (s0, []))
   end
 
-fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
-fun check ctxt = check' ctxt Property.stats
-fun checks ctxt = cpsCheck ctxt Property.stats
+fun check' context s0 = cpsCheck context s0 (fn _ => [])
+fun check context = check' context Property.stats
+fun checks context = cpsCheck context Property.stats
 
-fun checkGen ctxt (gen, show) (tag, prop) =
-  check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream
+fun checkGen context (gen, show) (tag, prop) =
+  check' context {count=0, tags=[("__GEN", 0)]} (limit context gen, show) (tag, prop) Generator.stream
 
-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 checkGenShrink context shrink (gen, show) (tag, prop) =
+  cpsCheck context {count=0, tags=[("__GEN", 0)]} shrink
+    (limit context gen, show) (tag, prop) Generator.stream
 
-fun checkOne ctxt show (tag, prop) obj =
-  check ctxt (List.getItem, show) (tag, prop) [obj]
+fun checkOne context show (tag, prop) obj =
+  check context (List.getItem, show) (tag, prop) [obj]
 
-(*calls the compiler and passes resulting type string to the parser*)
-fun determine_type context s =
+(*call the compiler and pass resulting type string to the parser*)
+fun determine_type ctxt s =
   let
     val ret = Unsynchronized.ref "return"
-    val ctx : use_context = {
+    val use_context : use_context = {
       tune_source = ML_Parse.fix_ints,
       name_space = ML_Env.name_space,
       str_of_pos = Position.here oo Position.line_file,
       print = fn r => ret := r,
       error = error
       }
-    val _ = context |> Context.proof_map
-      (ML_Context.exec (fn () => Secure.use_text ctx (0, "generated code") true s))
+    val _ = ctxt |> Context.proof_map
+      (ML_Context.exec (fn () => Secure.use_text use_context (0, "generated code") true s))
   in
     Gen_Construction.parse_pred (!ret)
   end;
 
-(*calls the compiler and runs the test*)
-fun run_test context s =
+(*call the compiler and run the test*)
+fun run_test ctxt s =
   let
     val _ =
       Context.proof_map
         (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code")
-        true s)) context
+        true s)) ctxt
   in () end;
 
 (*split input into tokens*)
@@ -170,21 +171,21 @@
     val (params, _) = Scan.finite stop p split
   in "fn (" ^ commas params ^ ") => " ^ code end;
 
-(*reads input and performs the test*)
-fun gen_check_property check context s =
+(*read input and perform the test*)
+fun gen_check_property check ctxt s =
   let
     val func = make_fun s
-    val (_, ty) = determine_type context func
-  in run_test context (check (Proof_Context.theory_of context) "Check" (ty, func)) end;
+    val (_, ty) = determine_type ctxt func
+  in run_test ctxt (check (Proof_Context.theory_of 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*)
 
-(*performs test for specification function*)
-fun gen_check_property_f check context s =
+(*perform test for specification function*)
+fun gen_check_property_f check ctxt s =
   let
-    val (name, ty) = determine_type context s
-  in run_test context (check (Proof_Context.theory_of context) name (ty, s)) end;
+    val (name, ty) = determine_type ctxt s
+  in run_test ctxt (check (Proof_Context.theory_of 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*)