48 |
48 |
49 type output_style = Context.generic -> string -> |
49 type output_style = Context.generic -> string -> |
50 {status: string option * Property.result * (Property.stats * string option list) -> unit, |
50 {status: string option * Property.result * (Property.stats * string option list) -> unit, |
51 finish: Property.stats * string option list -> unit} |
51 finish: Property.stats * string option list -> unit} |
52 |
52 |
53 fun limit ctxt gen = Generator.limit (Config.get_generic ctxt gen_max) gen |
53 fun limit context gen = Generator.limit (Config.get_generic context gen_max) gen |
54 |
54 |
55 structure Style = Theory_Data |
55 structure Style = Theory_Data |
56 ( |
56 ( |
57 type T = output_style Symtab.table |
57 type T = output_style Symtab.table |
58 val empty = Symtab.empty |
58 val empty = Symtab.empty |
59 val extend = I |
59 val extend = I |
60 fun merge data : T = Symtab.merge (K true) data |
60 fun merge data : T = Symtab.merge (K true) data |
61 ) |
61 ) |
62 |
62 |
63 fun get_style ctxt = |
63 fun get_style context = |
64 let val name = Config.get_generic ctxt style |
64 let val name = Config.get_generic context style |
65 in case Symtab.lookup (Style.get (Context.theory_of ctxt)) name of |
65 in case Symtab.lookup (Style.get (Context.theory_of context)) name of |
66 SOME style => style ctxt |
66 SOME style => style context |
67 | NONE => error ("No style called " ^ quote name ^ " found") |
67 | NONE => error ("No style called " ^ quote name ^ " found") |
68 end |
68 end |
69 |
69 |
70 fun register_style (name, style) = Style.map (Symtab.update (name, style)) |
70 fun register_style (name, style) = Style.map (Symtab.update (name, style)) |
71 |
71 |
|
72 |
72 (* testing functions *) |
73 (* testing functions *) |
73 |
74 |
74 fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) = |
75 fun cpsCheck context s0 shrink (next, show) (tag, prop) = |
75 let |
76 let |
76 val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f |
77 val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f |
77 |
78 |
78 val {status, finish} = get_style ctxt tag |
79 val {status, finish} = get_style context tag |
79 fun status' (obj, result, (stats, badobjs)) = |
80 fun status' (obj, result, (stats, badobjs)) = |
80 let |
81 let |
81 val badobjs' = if Property.failure result then obj :: badobjs else badobjs |
82 val badobjs' = if Property.failure result then obj :: badobjs else badobjs |
82 val _ = status (apply_show obj, result, (stats, map apply_show badobjs')) |
83 val _ = status (apply_show obj, result, (stats, map apply_show badobjs')) |
83 in badobjs' end |
84 in badobjs' end |
93 | NONE => status' (obj, result, (stats', badobjs)) |
94 | NONE => status' (obj, result, (stats', badobjs)) |
94 end |
95 end |
95 |
96 |
96 fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs) |
97 fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs) |
97 | iter (SOME (obj, stream), (stats, badobjs)) = |
98 | iter (SOME (obj, stream), (stats, badobjs)) = |
98 if #count stats >= Config.get_generic ctxt gen_target then |
99 if #count stats >= Config.get_generic context gen_target then |
99 finish (stats, map apply_show badobjs) |
100 finish (stats, map apply_show badobjs) |
100 else |
101 else |
101 let |
102 let |
102 val (result, stats') = Property.test prop (obj, stats) |
103 val (result, stats') = Property.test prop (obj, stats) |
103 val badobjs' = if Property.failure result then |
104 val badobjs' = if Property.failure result then |
107 in iter (next stream, (stats', badobjs')) end |
108 in iter (next stream, (stats', badobjs')) end |
108 in |
109 in |
109 fn stream => iter (next stream, (s0, [])) |
110 fn stream => iter (next stream, (s0, [])) |
110 end |
111 end |
111 |
112 |
112 fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => []) |
113 fun check' context s0 = cpsCheck context s0 (fn _ => []) |
113 fun check ctxt = check' ctxt Property.stats |
114 fun check context = check' context Property.stats |
114 fun checks ctxt = cpsCheck ctxt Property.stats |
115 fun checks context = cpsCheck context Property.stats |
115 |
116 |
116 fun checkGen ctxt (gen, show) (tag, prop) = |
117 fun checkGen context (gen, show) (tag, prop) = |
117 check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream |
118 check' context {count=0, tags=[("__GEN", 0)]} (limit context gen, show) (tag, prop) Generator.stream |
118 |
119 |
119 fun checkGenShrink ctxt shrink (gen, show) (tag, prop) = |
120 fun checkGenShrink context shrink (gen, show) (tag, prop) = |
120 cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink |
121 cpsCheck context {count=0, tags=[("__GEN", 0)]} shrink |
121 (limit ctxt gen, show) (tag, prop) Generator.stream |
122 (limit context gen, show) (tag, prop) Generator.stream |
122 |
123 |
123 fun checkOne ctxt show (tag, prop) obj = |
124 fun checkOne context show (tag, prop) obj = |
124 check ctxt (List.getItem, show) (tag, prop) [obj] |
125 check context (List.getItem, show) (tag, prop) [obj] |
125 |
126 |
126 (*calls the compiler and passes resulting type string to the parser*) |
127 (*call the compiler and pass resulting type string to the parser*) |
127 fun determine_type context s = |
128 fun determine_type ctxt s = |
128 let |
129 let |
129 val ret = Unsynchronized.ref "return" |
130 val ret = Unsynchronized.ref "return" |
130 val ctx : use_context = { |
131 val use_context : use_context = { |
131 tune_source = ML_Parse.fix_ints, |
132 tune_source = ML_Parse.fix_ints, |
132 name_space = ML_Env.name_space, |
133 name_space = ML_Env.name_space, |
133 str_of_pos = Position.here oo Position.line_file, |
134 str_of_pos = Position.here oo Position.line_file, |
134 print = fn r => ret := r, |
135 print = fn r => ret := r, |
135 error = error |
136 error = error |
136 } |
137 } |
137 val _ = context |> Context.proof_map |
138 val _ = ctxt |> Context.proof_map |
138 (ML_Context.exec (fn () => Secure.use_text ctx (0, "generated code") true s)) |
139 (ML_Context.exec (fn () => Secure.use_text use_context (0, "generated code") true s)) |
139 in |
140 in |
140 Gen_Construction.parse_pred (!ret) |
141 Gen_Construction.parse_pred (!ret) |
141 end; |
142 end; |
142 |
143 |
143 (*calls the compiler and runs the test*) |
144 (*call the compiler and run the test*) |
144 fun run_test context s = |
145 fun run_test ctxt s = |
145 let |
146 let |
146 val _ = |
147 val _ = |
147 Context.proof_map |
148 Context.proof_map |
148 (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") |
149 (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") |
149 true s)) context |
150 true s)) ctxt |
150 in () end; |
151 in () end; |
151 |
152 |
152 (*split input into tokens*) |
153 (*split input into tokens*) |
153 fun input_split s = |
154 fun input_split s = |
154 let |
155 let |
168 val (split, code) = input_split s |
169 val (split, code) = input_split s |
169 val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); |
170 val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); |
170 val (params, _) = Scan.finite stop p split |
171 val (params, _) = Scan.finite stop p split |
171 in "fn (" ^ commas params ^ ") => " ^ code end; |
172 in "fn (" ^ commas params ^ ") => " ^ code end; |
172 |
173 |
173 (*reads input and performs the test*) |
174 (*read input and perform the test*) |
174 fun gen_check_property check context s = |
175 fun gen_check_property check ctxt s = |
175 let |
176 let |
176 val func = make_fun s |
177 val func = make_fun s |
177 val (_, ty) = determine_type context func |
178 val (_, ty) = determine_type ctxt func |
178 in run_test context (check (Proof_Context.theory_of context) "Check" (ty, func)) end; |
179 in run_test ctxt (check (Proof_Context.theory_of ctxt) "Check" (ty, func)) end; |
179 |
180 |
180 val check_property = gen_check_property Gen_Construction.build_check |
181 val check_property = gen_check_property Gen_Construction.build_check |
181 (*val check_property_safe = gen_check_property Gen_Construction.safe_check*) |
182 (*val check_property_safe = gen_check_property Gen_Construction.safe_check*) |
182 |
183 |
183 (*performs test for specification function*) |
184 (*perform test for specification function*) |
184 fun gen_check_property_f check context s = |
185 fun gen_check_property_f check ctxt s = |
185 let |
186 let |
186 val (name, ty) = determine_type context s |
187 val (name, ty) = determine_type ctxt s |
187 in run_test context (check (Proof_Context.theory_of context) name (ty, s)) end; |
188 in run_test ctxt (check (Proof_Context.theory_of ctxt) name (ty, s)) end; |
188 |
189 |
189 val check_property_f = gen_check_property_f Gen_Construction.build_check |
190 val check_property_f = gen_check_property_f Gen_Construction.build_check |
190 (*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*) |
191 (*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*) |
191 |
192 |
192 end; |
193 end; |