--- 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
--- 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
--- 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*)