# HG changeset patch # User wenzelm # Date 1369942134 -7200 # Node ID 994055f7db80b4a0b15f81ae46b484912dee9566 # Parent afca6a99a361c04bb3a5c2ebd6474b358cbea8e1 simplified context and data management -- plain ctxt: Proof.context is default for most operations; diff -r afca6a99a361 -r 994055f7db80 src/HOL/Spec_Check/Spec_Check.thy --- 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 diff -r afca6a99a361 -r 994055f7db80 src/HOL/Spec_Check/gen_construction.ML --- 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; diff -r afca6a99a361 -r 994055f7db80 src/HOL/Spec_Check/generator.ML --- 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 *) diff -r afca6a99a361 -r 994055f7db80 src/HOL/Spec_Check/output_style.ML --- 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 diff -r afca6a99a361 -r 994055f7db80 src/HOL/Spec_Check/spec_check.ML --- 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*)