author  berghofe 
Thu, 10 Jan 2008 19:28:02 +0100  
changeset 25892  3ff9d646a66a 
parent 25400  e05b9fa43885 
child 26385  ae7564661e76 
permissions  rwrr 
11520  1 
(* Title: Pure/codegen.ML 
2 
ID: $Id$ 

11539  3 
Author: Stefan Berghofer, TU Muenchen 
11520  4 

11539  5 
Generic code generator. 
11520  6 
*) 
7 

8 
signature CODEGEN = 

9 
sig 

10 
val quiet_mode : bool ref 

11 
val message : string > unit 

13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

12 
val mode : string list ref 
13886
0b243f6e257e
Margin for prettyprinting is now a mutable reference.
berghofe
parents:
13753
diff
changeset

13 
val margin : int ref 
11520  14 

12452  15 
datatype 'a mixfix = 
11520  16 
Arg 
17 
 Ignore 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

18 
 Module 
11520  19 
 Pretty of Pretty.T 
12452  20 
 Quote of 'a; 
11520  21 

16649  22 
type deftab 
17144  23 
type node 
16649  24 
type codegr 
12452  25 
type 'a codegen 
26 

27 
val add_codegen: string > term codegen > theory > theory 

28 
val add_tycodegen: string > typ codegen > theory > theory 

15261  29 
val add_preprocessor: (theory > thm list > thm list) > theory > theory 
30 
val preprocess: theory > thm list > thm list 

17549  31 
val preprocess_term: theory > term > term 
11520  32 
val print_codegens: theory > unit 
17144  33 
val generate_code: theory > string list > string > (string * string) list > 
34 
(string * string) list * codegr 

35 
val generate_code_i: theory > string list > string > (string * term) list > 

36 
(string * string) list * codegr 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

37 
val assoc_const: string * (term mixfix list * 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

38 
(string * string) list) > theory > theory 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

39 
val assoc_const_i: (string * typ) * (term mixfix list * 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

40 
(string * string) list) > theory > theory 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

41 
val assoc_type: xstring * (typ mixfix list * 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

42 
(string * string) list) > theory > theory 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

43 
val get_assoc_code: theory > string * typ > 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

44 
(term mixfix list * (string * string) list) option 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

45 
val get_assoc_type: theory > string > 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

46 
(typ mixfix list * (string * string) list) option 
17144  47 
val codegen_error: codegr > string > string > 'a 
16649  48 
val invoke_codegen: theory > deftab > string > string > bool > 
49 
codegr * term > codegr * Pretty.T 

50 
val invoke_tycodegen: theory > deftab > string > string > bool > 

51 
codegr * typ > codegr * Pretty.T 

14858  52 
val mk_id: string > string 
17144  53 
val mk_qual_id: string > string * string > string 
54 
val mk_const_id: string > string > codegr > codegr * (string * string) 

55 
val get_const_id: string > codegr > string * string 

56 
val mk_type_id: string > string > codegr > codegr * (string * string) 

57 
val get_type_id: string > codegr > string * string 

16649  58 
val thyname_of_type: string > theory > string 
59 
val thyname_of_const: string > theory > string 

60 
val rename_terms: term list > term list 

11520  61 
val rename_term: term > term 
15398  62 
val new_names: term > string list > string list 
63 
val new_name: term > string > string 

17144  64 
val if_library: 'a > 'a > 'a 
16649  65 
val get_defn: theory > deftab > string > typ > 
66 
((typ * (string * (term list * term))) * int option) option 

24908
c74ad8782eeb
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24867
diff
changeset

67 
val is_instance: typ > typ > bool 
11520  68 
val parens: Pretty.T > Pretty.T 
69 
val mk_app: bool > Pretty.T > Pretty.T list > Pretty.T 

25892
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

70 
val mk_tuple: Pretty.T list > Pretty.T 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

71 
val mk_let: (Pretty.T * Pretty.T) list > Pretty.T > Pretty.T 
11520  72 
val eta_expand: term > term list > int > term 
14105  73 
val strip_tname: string > string 
13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

74 
val mk_type: bool > typ > Pretty.T 
17144  75 
val mk_term_of: codegr > string > bool > typ > Pretty.T 
76 
val mk_gen: codegr > string > bool > string list > string > typ > Pretty.T 

14105  77 
val test_fn: (int > (string * term) list option) ref 
24456  78 
val test_term: theory > bool > int > int > term > (string * term) list option 
79 
val auto_quickcheck: bool ref 

24805
34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

80 
val auto_quickcheck_time_limit: int ref 
24655
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

81 
val eval_result: (unit > term) ref 
17549  82 
val eval_term: theory > term > term 
20599  83 
val evaluation_conv: cterm > thm 
12452  84 
val parse_mixfix: (string > 'a) > string > 'a mixfix list 
18102  85 
val quotes_of: 'a mixfix list > 'a list 
18281  86 
val num_args_of: 'a mixfix list > int 
18102  87 
val replace_quotes: 'b list > 'a mixfix list > 'b mixfix list 
16649  88 
val mk_deftab: theory > deftab 
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19299
diff
changeset

89 
val add_unfold: thm > theory > theory 
17549  90 

17144  91 
val get_node: codegr > string > node 
92 
val add_edge: string * string > codegr > codegr 

93 
val add_edge_acyclic: string * string > codegr > codegr 

94 
val del_nodes: string list > codegr > codegr 

95 
val map_node: string > (node > node) > codegr > codegr 

96 
val new_node: string * node > codegr > codegr 

11520  97 
end; 
98 

99 
structure Codegen : CODEGEN = 

100 
struct 

101 

102 
val quiet_mode = ref true; 

103 
fun message s = if !quiet_mode then () else writeln s; 

104 

13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

105 
val mode = ref ([] : string list); 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

106 

13886
0b243f6e257e
Margin for prettyprinting is now a mutable reference.
berghofe
parents:
13753
diff
changeset

107 
val margin = ref 80; 
0b243f6e257e
Margin for prettyprinting is now a mutable reference.
berghofe
parents:
13753
diff
changeset

108 

11520  109 
(**** Mixfix syntax ****) 
110 

12452  111 
datatype 'a mixfix = 
11520  112 
Arg 
113 
 Ignore 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

114 
 Module 
11520  115 
 Pretty of Pretty.T 
12452  116 
 Quote of 'a; 
11520  117 

118 
fun is_arg Arg = true 

119 
 is_arg Ignore = true 

120 
 is_arg _ = false; 

121 

12452  122 
fun quotes_of [] = [] 
123 
 quotes_of (Quote q :: ms) = q :: quotes_of ms 

124 
 quotes_of (_ :: ms) = quotes_of ms; 

125 

126 
fun args_of [] xs = ([], xs) 

127 
 args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs) 

128 
 args_of (Ignore :: ms) (_ :: xs) = args_of ms xs 

129 
 args_of (_ :: ms) xs = args_of ms xs; 

11520  130 

18281  131 
fun num_args_of x = length (List.filter is_arg x); 
11520  132 

133 

134 
(**** theory data ****) 

135 

16649  136 
(* preprocessed definition table *) 
137 

138 
type deftab = 

139 
(typ * (* type of constant *) 

140 
(string * (* name of theory containing definition of constant *) 

141 
(term list * (* parameters *) 

142 
term))) (* righthand side *) 

143 
list Symtab.table; 

144 

145 
(* code dependency graph *) 

146 

17144  147 
type nametab = (string * string) Symtab.table * unit Symtab.table; 
148 

149 
fun merge_nametabs ((tab, used), (tab', used')) = 

150 
(Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used')); 

151 

152 
type node = 

16649  153 
(exn option * (* slot for arbitrary data *) 
154 
string * (* name of structure containing piece of code *) 

17144  155 
string); (* piece of code *) 
156 

157 
type codegr = 

158 
node Graph.T * 

159 
(nametab * (* table for assigned constant names *) 

160 
nametab); (* table for assigned type names *) 

161 

162 
val emptygr : codegr = (Graph.empty, 

163 
((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty))); 

16649  164 

14105  165 
(* type of code generators *) 
11520  166 

16649  167 
type 'a codegen = 
168 
theory > (* theory in which generate_code was called *) 

169 
deftab > (* definition table (for efficiency) *) 

170 
codegr > (* code dependency graph *) 

171 
string > (* node name of caller (for recording dependencies) *) 

17144  172 
string > (* module name of caller (for modular code generation) *) 
16649  173 
bool > (* whether to parenthesize generated expression *) 
174 
'a > (* item to generate code from *) 

175 
(codegr * Pretty.T) option; 

12452  176 

14105  177 
(* parameters for random testing *) 
178 

179 
type test_params = 

180 
{size: int, iterations: int, default_type: typ option}; 

181 

182 
fun merge_test_params 

183 
{size = size1, iterations = iterations1, default_type = default_type1} 

184 
{size = size2, iterations = iterations2, default_type = default_type2} = 

185 
{size = Int.max (size1, size2), 

186 
iterations = Int.max (iterations1, iterations2), 

187 
default_type = case default_type1 of 

15531  188 
NONE => default_type2 
14105  189 
 _ => default_type1}; 
190 

191 
val default_test_params : test_params = 

15531  192 
{size = 10, iterations = 100, default_type = NONE}; 
14105  193 

194 
fun set_size size ({iterations, default_type, ...} : test_params) = 

195 
{size = size, iterations = iterations, default_type = default_type}; 

196 

197 
fun set_iterations iterations ({size, default_type, ...} : test_params) = 

198 
{size = size, iterations = iterations, default_type = default_type}; 

199 

16458  200 
fun set_default_type s thy ({size, iterations, ...} : test_params) = 
14105  201 
{size = size, iterations = iterations, 
24707  202 
default_type = SOME (Syntax.read_typ_global thy s)}; 
14105  203 

22846  204 

205 
(* theory data *) 

16458  206 

207 
structure CodegenData = TheoryDataFun 

22846  208 
( 
11520  209 
type T = 
12452  210 
{codegens : (string * term codegen) list, 
211 
tycodegens : (string * typ codegen) list, 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

212 
consts : ((string * typ) * (term mixfix list * (string * string) list)) list, 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

213 
types : (string * (typ mixfix list * (string * string) list)) list, 
15261  214 
preprocs: (stamp * (theory > thm list > thm list)) list, 
17144  215 
modules: codegr Symtab.table, 
14105  216 
test_params: test_params}; 
11520  217 

12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

218 
val empty = 
24219  219 
{codegens = [], tycodegens = [], consts = [], types = [], 
17144  220 
preprocs = [], modules = Symtab.empty, test_params = default_test_params}; 
11520  221 
val copy = I; 
16458  222 
val extend = I; 
11520  223 

16458  224 
fun merge _ 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

225 
({codegens = codegens1, tycodegens = tycodegens1, 
24219  226 
consts = consts1, types = types1, 
17144  227 
preprocs = preprocs1, modules = modules1, test_params = test_params1}, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

228 
{codegens = codegens2, tycodegens = tycodegens2, 
24219  229 
consts = consts2, types = types2, 
17144  230 
preprocs = preprocs2, modules = modules2, test_params = test_params2}) = 
19119
dea8d858d37f
abandoned merge_alists' in favour of generic AList.merge
haftmann
parents:
19046
diff
changeset

231 
{codegens = AList.merge (op =) (K true) (codegens1, codegens2), 
dea8d858d37f
abandoned merge_alists' in favour of generic AList.merge
haftmann
parents:
19046
diff
changeset

232 
tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2), 
21098
d0d8a48ae4e6
switched merge_alists'' to AList.merge'' whenever appropriate
haftmann
parents:
21056
diff
changeset

233 
consts = AList.merge (op =) (K true) (consts1, consts2), 
d0d8a48ae4e6
switched merge_alists'' to AList.merge'' whenever appropriate
haftmann
parents:
21056
diff
changeset

234 
types = AList.merge (op =) (K true) (types1, types2), 
19119
dea8d858d37f
abandoned merge_alists' in favour of generic AList.merge
haftmann
parents:
19046
diff
changeset

235 
preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2), 
17144  236 
modules = Symtab.merge (K true) (modules1, modules2), 
14105  237 
test_params = merge_test_params test_params1 test_params2}; 
22846  238 
); 
11520  239 

22846  240 
fun print_codegens thy = 
241 
let val {codegens, tycodegens, ...} = CodegenData.get thy in 

12452  242 
Pretty.writeln (Pretty.chunks 
243 
[Pretty.strs ("term code generators:" :: map fst codegens), 

22846  244 
Pretty.strs ("type code generators:" :: map fst tycodegens)]) 
245 
end; 

11520  246 

247 

248 

14105  249 
(**** access parameters for random testing ****) 
250 

251 
fun get_test_params thy = #test_params (CodegenData.get thy); 

252 

253 
fun map_test_params f thy = 

24219  254 
let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
14105  255 
CodegenData.get thy; 
256 
in CodegenData.put {codegens = codegens, tycodegens = tycodegens, 

24219  257 
consts = consts, types = types, preprocs = preprocs, 
17144  258 
modules = modules, test_params = f test_params} thy 
259 
end; 

260 

261 

262 
(**** access modules ****) 

263 

264 
fun get_modules thy = #modules (CodegenData.get thy); 

265 

266 
fun map_modules f thy = 

24219  267 
let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
17144  268 
CodegenData.get thy; 
269 
in CodegenData.put {codegens = codegens, tycodegens = tycodegens, 

24219  270 
consts = consts, types = types, preprocs = preprocs, 
17144  271 
modules = f modules, test_params = test_params} thy 
14105  272 
end; 
273 

274 

12452  275 
(**** add new code generators to theory ****) 
11520  276 

277 
fun add_codegen name f thy = 

24219  278 
let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
14105  279 
CodegenData.get thy 
17521  280 
in (case AList.lookup (op =) codegens name of 
15531  281 
NONE => CodegenData.put {codegens = (name, f) :: codegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

282 
tycodegens = tycodegens, consts = consts, types = types, 
24219  283 
preprocs = preprocs, modules = modules, 
17144  284 
test_params = test_params} thy 
15531  285 
 SOME _ => error ("Code generator " ^ name ^ " already declared")) 
12452  286 
end; 
287 

288 
fun add_tycodegen name f thy = 

24219  289 
let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
14105  290 
CodegenData.get thy 
17521  291 
in (case AList.lookup (op =) tycodegens name of 
15531  292 
NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

293 
codegens = codegens, consts = consts, types = types, 
24219  294 
preprocs = preprocs, modules = modules, 
17144  295 
test_params = test_params} thy 
15531  296 
 SOME _ => error ("Code generator " ^ name ^ " already declared")) 
11520  297 
end; 
298 

299 

15261  300 
(**** preprocessors ****) 
301 

302 
fun add_preprocessor p thy = 

24219  303 
let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
15261  304 
CodegenData.get thy 
305 
in CodegenData.put {tycodegens = tycodegens, 

306 
codegens = codegens, consts = consts, types = types, 

24219  307 
preprocs = (stamp (), p) :: preprocs, 
17144  308 
modules = modules, test_params = test_params} thy 
15261  309 
end; 
310 

21836  311 
fun preprocess thy = 
15261  312 
let val {preprocs, ...} = CodegenData.get thy 
21836  313 
in fold (fn (_, f) => f thy) preprocs end; 
15261  314 

17549  315 
fun preprocess_term thy t = 
316 
let 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset

317 
val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t); 
17549  318 
(* fake definition *) 
319 
val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) 

320 
(Logic.mk_equals (x, t)); 

321 
fun err () = error "preprocess_term: bad preprocessor" 

322 
in case map prop_of (preprocess thy [eq]) of 

323 
[Const ("==", _) $ x' $ t'] => if x = x' then t' else err () 

324 
 _ => err () 

325 
end; 

18281  326 

19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19299
diff
changeset

327 
fun add_unfold eqn = 
15261  328 
let 
22749  329 
val thy = Thm.theory_of_thm eqn; 
330 
val ctxt = ProofContext.init thy; 

331 
val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn; 

332 
val names = term_consts (fst (Logic.dest_equals (prop_of eqn'))); 

15261  333 
fun prep thy = map (fn th => 
17666  334 
let val prop = prop_of th 
335 
in 

336 
if forall (fn name => exists_Const (equal name o fst) prop) names 

22749  337 
then rewrite_rule [eqn'] (Thm.transfer thy th) 
17666  338 
else th 
339 
end) 

19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19299
diff
changeset

340 
in add_preprocessor prep end; 
15261  341 

24456  342 
val _ = Context.add_setup 
343 
(let 

344 
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); 

345 
in 

346 
Code.add_attribute ("unfold", Scan.succeed (mk_attribute 

347 
(fn thm => add_unfold thm #> Code.add_inline thm))) 

348 
end); 

22749  349 

15261  350 

11520  351 
(**** associate constants with target language code ****) 
352 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

353 
fun gen_assoc_const prep_const (raw_const, syn) thy = 
11520  354 
let 
24219  355 
val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
14105  356 
CodegenData.get thy; 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

357 
val (cname, T) = prep_const thy raw_const; 
11520  358 
in 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

359 
if num_args_of (fst syn) > length (binder_types T) then 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

360 
error ("More arguments than in corresponding type of " ^ cname) 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

361 
else case AList.lookup (op =) consts (cname, T) of 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

362 
NONE => CodegenData.put {codegens = codegens, 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

363 
tycodegens = tycodegens, 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

364 
consts = ((cname, T), syn) :: consts, 
24219  365 
types = types, preprocs = preprocs, 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

366 
modules = modules, test_params = test_params} thy 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

367 
 SOME _ => error ("Constant " ^ cname ^ " already associated with code") 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

368 
end; 
11520  369 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

370 
val assoc_const_i = gen_assoc_const (K I); 
24219  371 
val assoc_const = gen_assoc_const CodeUnit.read_bare_const; 
11520  372 

15801  373 

11520  374 
(**** associate types with target language types ****) 
375 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

376 
fun assoc_type (s, syn) thy = 
11520  377 
let 
24219  378 
val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = 
14105  379 
CodegenData.get thy; 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

380 
val tc = Sign.intern_type thy s; 
11520  381 
in 
18320
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

382 
case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

383 
SOME (Type.LogicalType i, _) => 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

384 
if num_args_of (fst syn) > i then 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

385 
error ("More arguments than corresponding type constructor " ^ s) 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

386 
else (case AList.lookup (op =) types tc of 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

387 
NONE => CodegenData.put {codegens = codegens, 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

388 
tycodegens = tycodegens, consts = consts, 
24219  389 
types = (tc, syn) :: types, 
18320
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

390 
preprocs = preprocs, modules = modules, test_params = test_params} thy 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

391 
 SOME _ => error ("Type " ^ tc ^ " already associated with code")) 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

392 
 _ => error ("Not a type constructor: " ^ s) 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

393 
end; 
11520  394 

21098
d0d8a48ae4e6
switched merge_alists'' to AList.merge'' whenever appropriate
haftmann
parents:
21056
diff
changeset

395 
fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy); 
11546  396 

11520  397 

398 
(**** make valid ML identifiers ****) 

399 

14858  400 
fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse 
401 
Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x; 

402 

403 
fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (explode s))) of 

404 
("<" :: "^" :: xs, ">") => (true, implode xs) 

405 
 ("<" :: xs, ">") => (false, implode xs) 

406 
 _ => sys_error "dest_sym"); 

16458  407 

14858  408 
fun mk_id s = if s = "" then "" else 
11520  409 
let 
14858  410 
fun check_str [] = [] 
411 
 check_str xs = (case take_prefix is_ascii_letdig xs of 

412 
([], " " :: zs) => check_str zs 

413 
 ([], z :: zs) => 

414 
if size z = 1 then string_of_int (ord z) :: check_str zs 

415 
else (case dest_sym z of 

416 
(true, "isub") => check_str zs 

417 
 (true, "isup") => "" :: check_str zs 

418 
 (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs) 

419 
 (ys, zs) => implode ys :: check_str zs); 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

420 
val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s)) 
11520  421 
in 
14858  422 
if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' 
11520  423 
end; 
424 

17144  425 
fun mk_long_id (p as (tab, used)) module s = 
16649  426 
let 
17144  427 
fun find_name [] = sys_error "mk_long_id" 
428 
 find_name (ys :: yss) = 

429 
let 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

430 
val s' = NameSpace.implode ys 
17144  431 
val s'' = NameSpace.append module s' 
17412  432 
in case Symtab.lookup used s'' of 
17261  433 
NONE => ((module, s'), 
17412  434 
(Symtab.update_new (s, (module, s')) tab, 
435 
Symtab.update_new (s'', ()) used)) 

17144  436 
 SOME _ => find_name yss 
437 
end 

17412  438 
in case Symtab.lookup tab s of 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

439 
NONE => find_name (Library.suffixes1 (NameSpace.explode s)) 
17144  440 
 SOME name => (name, p) 
16649  441 
end; 
442 

17144  443 
(* module: module name for caller *) 
444 
(* module': module name for callee *) 

445 
(* if caller and callee reside in different modules, use qualified access *) 

16649  446 

17144  447 
fun mk_qual_id module (module', s) = 
448 
if module = module' orelse module' = "" then s else module' ^ "." ^ s; 

449 

450 
fun mk_const_id module cname (gr, (tab1, tab2)) = 

16649  451 
let 
17144  452 
val ((module, s), tab1') = mk_long_id tab1 module cname 
453 
val s' = mk_id s; 

21478
a90250b1cf42
moved ML syntax operations to structure ML_Syntax;
wenzelm
parents:
21098
diff
changeset

454 
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s' 
17144  455 
in ((gr, (tab1', tab2)), (module, s'')) end; 
13073
cc9d7f403a4b
mk_const_id now checks for clashes with reserved ML identifiers.
berghofe
parents:
13003
diff
changeset

456 

17144  457 
fun get_const_id cname (gr, (tab1, tab2)) = 
17412  458 
case Symtab.lookup (fst tab1) cname of 
17144  459 
NONE => error ("get_const_id: no such constant: " ^ quote cname) 
460 
 SOME (module, s) => 

461 
let 

462 
val s' = mk_id s; 

21478
a90250b1cf42
moved ML syntax operations to structure ML_Syntax;
wenzelm
parents:
21098
diff
changeset

463 
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s' 
17144  464 
in (module, s'') end; 
465 

466 
fun mk_type_id module tyname (gr, (tab1, tab2)) = 

16649  467 
let 
17144  468 
val ((module, s), tab2') = mk_long_id tab2 module tyname 
469 
val s' = mk_id s; 

21478
a90250b1cf42
moved ML syntax operations to structure ML_Syntax;
wenzelm
parents:
21098
diff
changeset

470 
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s' 
17144  471 
in ((gr, (tab1, tab2')), (module, s'')) end; 
16649  472 

17144  473 
fun get_type_id tyname (gr, (tab1, tab2)) = 
17412  474 
case Symtab.lookup (fst tab2) tyname of 
17144  475 
NONE => error ("get_type_id: no such type: " ^ quote tyname) 
476 
 SOME (module, s) => 

477 
let 

478 
val s' = mk_id s; 

21478
a90250b1cf42
moved ML syntax operations to structure ML_Syntax;
wenzelm
parents:
21098
diff
changeset

479 
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s' 
17144  480 
in (module, s'') end; 
481 

482 
fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab); 

483 

484 
fun get_node (gr, x) k = Graph.get_node gr k; 

485 
fun add_edge e (gr, x) = (Graph.add_edge e gr, x); 

486 
fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x); 

487 
fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x); 

488 
fun map_node k f (gr, x) = (Graph.map_node k f gr, x); 

489 
fun new_node p (gr, x) = (Graph.new_node p gr, x); 

16649  490 

18281  491 
fun theory_of_type s thy = 
16649  492 
if Sign.declared_tyname thy s 
19473  493 
then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy))) 
16649  494 
else NONE; 
495 

18281  496 
fun theory_of_const s thy = 
16649  497 
if Sign.declared_const thy s 
19473  498 
then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy))) 
16649  499 
else NONE; 
500 

501 
fun thyname_of_type s thy = (case theory_of_type s thy of 

502 
NONE => error ("thyname_of_type: no such type: " ^ quote s) 

503 
 SOME thy' => Context.theory_name thy'); 

504 

505 
fun thyname_of_const s thy = (case theory_of_const s thy of 

506 
NONE => error ("thyname_of_const: no such constant: " ^ quote s) 

507 
 SOME thy' => Context.theory_name thy'); 

11520  508 

13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

509 
fun rename_terms ts = 
11520  510 
let 
23178  511 
val names = List.foldr add_term_names 
20286  512 
(map (fst o fst) (rev (fold Term.add_vars ts []))) ts; 
21478
a90250b1cf42
moved ML syntax operations to structure ML_Syntax;
wenzelm
parents:
21098
diff
changeset

513 
val reserved = filter ML_Syntax.is_reserved names; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

514 
val (illegal, alt_names) = split_list (map_filter (fn s => 
15531  515 
let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names) 
14858  516 
val ps = (reserved @ illegal) ~~ 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset

517 
Name.variant_list names (map (suffix "'") reserved @ alt_names); 
11520  518 

17521  519 
fun rename_id s = AList.lookup (op =) ps s > the_default s; 
14858  520 

521 
fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T) 

522 
 rename (Free (a, T)) = Free (rename_id a, T) 

11520  523 
 rename (Abs (s, T, t)) = Abs (s, T, rename t) 
524 
 rename (t $ u) = rename t $ rename u 

525 
 rename t = t; 

526 
in 

13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

527 
map rename ts 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

528 
end; 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

529 

e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

530 
val rename_term = hd o rename_terms o single; 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

531 

e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

532 

e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

533 
(**** retrieve definition of constant ****) 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

534 

24908
c74ad8782eeb
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24867
diff
changeset

535 
fun is_instance T1 T2 = 
c74ad8782eeb
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24867
diff
changeset

536 
Type.raw_instance (T1, Logic.legacy_varifyT T2); 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

537 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

538 
fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) => 
24908
c74ad8782eeb
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24867
diff
changeset

539 
s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

540 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

541 
fun get_aux_code xs = map_filter (fn (m, code) => 
20665  542 
if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

543 

16649  544 
fun mk_deftab thy = 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

545 
let 
22680
31a2303f4283
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

546 
val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy')) 
16649  547 
(thy :: Theory.ancestors_of thy); 
15261  548 
fun prep_def def = (case preprocess thy [def] of 
16649  549 
[def'] => prop_of def'  _ => error "mk_deftab: bad preprocessor"); 
15261  550 
fun dest t = 
551 
let 

552 
val (lhs, rhs) = Logic.dest_equals t; 

553 
val (c, args) = strip_comb lhs; 

16649  554 
val (s, T) = dest_Const c 
555 
in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE 

15531  556 
end handle TERM _ => NONE; 
21056  557 
fun add_def thyname (name, t) = (case dest t of 
558 
NONE => I 

24908
c74ad8782eeb
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24867
diff
changeset

559 
 SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of 
21056  560 
NONE => I 
561 
 SOME (s, (T, (args, rhs))) => Symtab.map_default (s, []) 

562 
(cons (T, (thyname, split_last (rename_terms (args @ [rhs]))))))) 

13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

563 
in 
21056  564 
fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty 
11520  565 
end; 
566 

17412  567 
fun get_defn thy defs s T = (case Symtab.lookup defs s of 
16649  568 
NONE => NONE 
569 
 SOME ds => 

24908
c74ad8782eeb
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24867
diff
changeset

570 
let val i = find_index (is_instance T o fst) ds 
16649  571 
in if i >= 0 then 
572 
SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) 

573 
else NONE 

574 
end); 

575 

11520  576 

12452  577 
(**** invoke suitable code generator for term / type ****) 
11520  578 

17144  579 
fun codegen_error (gr, _) dep s = 
580 
error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep])); 

581 

582 
fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first 

583 
(fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of 

584 
NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^ 

585 
Sign.string_of_term thy t) 

15531  586 
 SOME x => x); 
12452  587 

17144  588 
fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first 
589 
(fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of 

590 
NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^ 

591 
Sign.string_of_typ thy T) 

15531  592 
 SOME x => x); 
11520  593 

594 

595 
(**** code generator for mixfix expressions ****) 

596 

597 
fun parens p = Pretty.block [Pretty.str "(", p, Pretty.str ")"]; 

598 

599 
fun pretty_fn [] p = [p] 

600 
 pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") :: 

601 
Pretty.brk 1 :: pretty_fn xs p; 

602 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

603 
fun pretty_mixfix _ _ [] [] _ = [] 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

604 
 pretty_mixfix module module' (Arg :: ms) (p :: ps) qs = 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

605 
p :: pretty_mixfix module module' ms ps qs 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

606 
 pretty_mixfix module module' (Ignore :: ms) ps qs = 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

607 
pretty_mixfix module module' ms ps qs 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

608 
 pretty_mixfix module module' (Module :: ms) ps qs = 
17144  609 
(if module <> module' 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

610 
then cons (Pretty.str (module' ^ ".")) else I) 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

611 
(pretty_mixfix module module' ms ps qs) 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

612 
 pretty_mixfix module module' (Pretty p :: ms) ps qs = 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

613 
p :: pretty_mixfix module module' ms ps qs 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

614 
 pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) = 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

615 
q :: pretty_mixfix module module' ms ps qs; 
11520  616 

18102  617 
fun replace_quotes [] [] = [] 
618 
 replace_quotes xs (Arg :: ms) = 

619 
Arg :: replace_quotes xs ms 

620 
 replace_quotes xs (Ignore :: ms) = 

621 
Ignore :: replace_quotes xs ms 

622 
 replace_quotes xs (Module :: ms) = 

623 
Module :: replace_quotes xs ms 

624 
 replace_quotes xs (Pretty p :: ms) = 

625 
Pretty p :: replace_quotes xs ms 

626 
 replace_quotes (x::xs) (Quote _ :: ms) = 

627 
Quote x :: replace_quotes xs ms; 

628 

11520  629 

12452  630 
(**** default code generators ****) 
11520  631 

632 
fun eta_expand t ts i = 

633 
let 

24456  634 
val k = length ts; 
635 
val Ts = Library.drop (k, binder_types (fastype_of t)); 

636 
val j = i  k 

11520  637 
in 
23178  638 
List.foldr (fn (T, t) => Abs ("x", T, t)) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

639 
(list_comb (t, ts @ map Bound (j1 downto 0))) (Library.take (j, Ts)) 
11520  640 
end; 
641 

642 
fun mk_app _ p [] = p 

643 
 mk_app brack p ps = if brack then 

644 
Pretty.block (Pretty.str "(" :: 

645 
separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"]) 

646 
else Pretty.block (separate (Pretty.brk 1) (p :: ps)); 

647 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset

648 
fun new_names t xs = Name.variant_list 
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset

649 
(map (fst o fst o dest_Var) (term_vars t) union 
21719  650 
add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs); 
11520  651 

652 
fun new_name t x = hd (new_names t [x]); 

653 

20665  654 
fun if_library x y = if member (op =) (!mode) "library" then x else y; 
17144  655 

656 
fun default_codegen thy defs gr dep module brack t = 

11520  657 
let 
658 
val (u, ts) = strip_comb t; 

17144  659 
fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) 
11520  660 
in (case u of 
14105  661 
Var ((s, i), T) => 
662 
let 

663 
val (gr', ps) = codegens true (gr, ts); 

17144  664 
val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) 
15531  665 
in SOME (gr'', mk_app brack (Pretty.str (s ^ 
11520  666 
(if i=0 then "" else string_of_int i))) ps) 
667 
end 

668 

14105  669 
 Free (s, T) => 
670 
let 

671 
val (gr', ps) = codegens true (gr, ts); 

17144  672 
val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) 
15531  673 
in SOME (gr'', mk_app brack (Pretty.str s) ps) end 
11520  674 

675 
 Const (s, T) => 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

676 
(case get_assoc_code thy (s, T) of 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

677 
SOME (ms, aux) => 
18281  678 
let val i = num_args_of ms 
11520  679 
in if length ts < i then 
17144  680 
default_codegen thy defs gr dep module brack (eta_expand u ts i) 
11520  681 
else 
682 
let 

12452  683 
val (ts1, ts2) = args_of ms ts; 
684 
val (gr1, ps1) = codegens false (gr, ts1); 

685 
val (gr2, ps2) = codegens true (gr1, ts2); 

686 
val (gr3, ps3) = codegens false (gr2, quotes_of ms); 

17549  687 
val (gr4, _) = invoke_tycodegen thy defs dep module false 
688 
(gr3, funpow (length ts) (hd o tl o snd o dest_Type) T); 

17144  689 
val (module', suffix) = (case get_defn thy defs s T of 
690 
NONE => (if_library (thyname_of_const s thy) module, "") 

691 
 SOME ((U, (module', _)), NONE) => 

692 
(if_library module' module, "") 

693 
 SOME ((U, (module', _)), SOME i) => 

694 
(if_library module' module, " def" ^ string_of_int i)); 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

695 
val node_id = s ^ suffix; 
17144  696 
fun p module' = mk_app brack (Pretty.block 
697 
(pretty_mixfix module module' ms ps1 ps3)) ps2 

17549  698 
in SOME (case try (get_node gr4) node_id of 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

699 
NONE => (case get_aux_code aux of 
17549  700 
[] => (gr4, p module) 
17144  701 
 xs => (add_edge (node_id, dep) (new_node 
17549  702 
(node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4), 
17144  703 
p module')) 
704 
 SOME (_, module'', _) => 

17549  705 
(add_edge (node_id, dep) gr4, p module'')) 
11520  706 
end 
707 
end 

16649  708 
 NONE => (case get_defn thy defs s T of 
15531  709 
NONE => NONE 
17144  710 
 SOME ((U, (thyname, (args, rhs))), k) => 
11520  711 
let 
17144  712 
val module' = if_library thyname module; 
713 
val suffix = (case k of NONE => ""  SOME i => " def" ^ string_of_int i); 

16649  714 
val node_id = s ^ suffix; 
17144  715 
val (gr', (ps, def_id)) = codegens true (gr, ts) >>> 
716 
mk_const_id module' (s ^ suffix); 

717 
val p = mk_app brack (Pretty.str (mk_qual_id module def_id)) ps 

718 
in SOME (case try (get_node gr') node_id of 

719 
NONE => 

720 
let 

721 
val _ = message ("expanding definition of " ^ s); 

18788
4f4ed2a01152
Fixed bug in code generator for primitive definitions that
berghofe
parents:
18728
diff
changeset

722 
val (Ts, _) = strip_type U; 
17144  723 
val (args', rhs') = 
724 
if not (null args) orelse null Ts then (args, rhs) else 

725 
let val v = Free (new_name rhs "x", hd Ts) 

726 
in ([v], betapply (rhs, v)) end; 

727 
val (gr1, p') = invoke_codegen thy defs node_id module' false 

728 
(add_edge (node_id, dep) 

729 
(new_node (node_id, (NONE, "", "")) gr'), rhs'); 

730 
val (gr2, xs) = codegens false (gr1, args'); 

731 
val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T); 

732 
val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U); 

733 
in (map_node node_id (K (NONE, module', Pretty.string_of 

734 
(Pretty.block (separate (Pretty.brk 1) 

735 
(if null args' then 

736 
[Pretty.str ("val " ^ snd def_id ^ " :"), ty] 

737 
else Pretty.str ("fun " ^ snd def_id) :: xs) @ 

738 
[Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4, 

739 
p) 

740 
end 

741 
 SOME _ => (add_edge (node_id, dep) gr', p)) 

11520  742 
end)) 
743 

744 
 Abs _ => 

745 
let 

746 
val (bs, Ts) = ListPair.unzip (strip_abs_vars u); 

747 
val t = strip_abs_body u 

748 
val bs' = new_names t bs; 

12452  749 
val (gr1, ps) = codegens true (gr, ts); 
17144  750 
val (gr2, p) = invoke_codegen thy defs dep module false 
12452  751 
(gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); 
11520  752 
in 
15531  753 
SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ 
11520  754 
[Pretty.str ")"])) ps) 
755 
end 

756 

15531  757 
 _ => NONE) 
11520  758 
end; 
759 

17144  760 
fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) = 
15531  761 
SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i))) 
17144  762 
 default_tycodegen thy defs gr dep module brack (TFree (s, _)) = 
16649  763 
SOME (gr, Pretty.str s) 
17144  764 
 default_tycodegen thy defs gr dep module brack (Type (s, Ts)) = 
17521  765 
(case AList.lookup (op =) ((#types o CodegenData.get) thy) s of 
15531  766 
NONE => NONE 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

767 
 SOME (ms, aux) => 
12452  768 
let 
769 
val (gr', ps) = foldl_map 

17144  770 
(invoke_tycodegen thy defs dep module false) 
16649  771 
(gr, fst (args_of ms Ts)); 
12452  772 
val (gr'', qs) = foldl_map 
17144  773 
(invoke_tycodegen thy defs dep module false) 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

774 
(gr', quotes_of ms); 
17144  775 
val module' = if_library (thyname_of_type s thy) module; 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

776 
val node_id = s ^ " (type)"; 
17144  777 
fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) 
778 
in SOME (case try (get_node gr'') node_id of 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

779 
NONE => (case get_aux_code aux of 
17144  780 
[] => (gr'', p module') 
781 
 xs => (fst (mk_type_id module' s 

782 
(add_edge (node_id, dep) (new_node (node_id, 

783 
(NONE, module', space_implode "\n" xs ^ "\n")) gr''))), 

784 
p module')) 

785 
 SOME (_, module'', _) => 

786 
(add_edge (node_id, dep) gr'', p module'')) 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

787 
end); 
12452  788 

24456  789 
val _ = Context.add_setup 
790 
(add_codegen "default" default_codegen #> 

791 
add_tycodegen "default" default_tycodegen); 

792 

793 

25892
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

794 
fun mk_tuple [p] = p 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

795 
 mk_tuple ps = Pretty.block (Pretty.str "(" :: 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

796 
List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single ps)) @ 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

797 
[Pretty.str ")"]); 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

798 

3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

799 
fun mk_let bindings body = 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

800 
Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

801 
Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) => 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

802 
Pretty.block [Pretty.str "val ", pat, Pretty.str " =", Pretty.brk 1, 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

803 
rhs, Pretty.str ";"]) bindings)), 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

804 
Pretty.brk 1, Pretty.str "in", Pretty.brk 1, body, 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

805 
Pretty.brk 1, Pretty.str "end"]); 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

806 

16649  807 
fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n"; 
808 

17521  809 
fun add_to_module name s = AList.map_entry (op =) name (suffix s); 
16649  810 

17144  811 
fun output_code gr module xs = 
16649  812 
let 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

813 
val code = map_filter (fn s => 
17144  814 
let val c as (_, module', _) = Graph.get_node gr s 
815 
in if module = "" orelse module = module' then SOME (s, c) else NONE end) 

816 
(rev (Graph.all_preds gr xs)); 

16649  817 
fun string_of_cycle (a :: b :: cs) = 
818 
let val SOME (x, y) = get_first (fn (x, (_, a', _)) => 

819 
if a = a' then Option.map (pair x) 

21056  820 
(find_first (equal b o #2 o Graph.get_node gr) 
16649  821 
(Graph.imm_succs gr x)) 
822 
else NONE) code 

823 
in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end 

824 
 string_of_cycle _ = "" 

825 
in 

17144  826 
if module = "" then 
16649  827 
let 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18977
diff
changeset

828 
val modules = distinct (op =) (map (#2 o snd) code); 
23178  829 
val mod_gr = fold_rev Graph.add_edge_acyclic 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

830 
(maps (fn (s, (_, module, _)) => map (pair module) 
17144  831 
(filter_out (equal module) (map (#2 o Graph.get_node gr) 
23178  832 
(Graph.imm_succs gr s)))) code) 
833 
(fold_rev (Graph.new_node o rpair ()) modules Graph.empty); 

16649  834 
val modules' = 
835 
rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) 

836 
in 

23178  837 
List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms) 
16649  838 
(map (rpair "") modules') code 
839 
end handle Graph.CYCLES (cs :: _) => 

840 
error ("Cyclic dependency of modules:\n" ^ commas cs ^ 

841 
"\n" ^ string_of_cycle cs) 

17144  842 
else [(module, implode (map (#3 o snd) code))] 
16649  843 
end; 
11520  844 

17144  845 
fun gen_generate_code prep_term thy modules module = 
24634  846 
PrintMode.setmp [] (Pretty.setmp_margin (!margin) (fn xs => 
11520  847 
let 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

848 
val _ = (module <> "" orelse 
20665  849 
member (op =) (!mode) "library" andalso forall (equal "" o fst) xs) 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

850 
orelse error "missing module name"; 
17144  851 
val graphs = get_modules thy; 
16649  852 
val defs = mk_deftab thy; 
17144  853 
val gr = new_node ("<Top>", (NONE, module, "")) 
23178  854 
(List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => 
17144  855 
(Graph.merge (fn ((_, module, _), (_, module', _)) => 
856 
module = module') (gr, gr'), 

857 
(merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr 

17412  858 
(map (fn s => case Symtab.lookup graphs s of 
17144  859 
NONE => error ("Undefined code module: " ^ s) 
860 
 SOME gr => gr) modules)) 

23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23178
diff
changeset

861 
handle Graph.DUP k => error ("Duplicate code for " ^ k); 
16649  862 
fun expand (t as Abs _) = t 
863 
 expand t = (case fastype_of t of 

864 
Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0)  _ => t); 

11520  865 
val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) 
17144  866 
(invoke_codegen thy defs "<Top>" module false (gr, t))) 
17549  867 
(gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

868 
val code = map_filter 
17144  869 
(fn ("", _) => NONE 
870 
 (s', p) => SOME (Pretty.string_of (Pretty.block 

871 
[Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps; 

872 
val code' = space_implode "\n\n" code ^ "\n\n"; 

873 
val code'' = 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

874 
map_filter (fn (name, s) => 
20665  875 
if member (op =) (!mode) "library" andalso name = module andalso null code 
17144  876 
then NONE 
877 
else SOME (name, mk_struct name s)) 

878 
((if null code then I 

879 
else add_to_module module code') 

880 
(output_code (fst gr') (if_library "" module) ["<Top>"])) 

16649  881 
in 
17144  882 
(code'', del_nodes ["<Top>"] gr') 
16649  883 
end)); 
11520  884 

22680
31a2303f4283
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

885 
val generate_code_i = gen_generate_code Sign.cert_term; 
31a2303f4283
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

886 
val generate_code = gen_generate_code Sign.read_term; 
11520  887 

12452  888 

13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

889 
(**** Reflection ****) 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

890 

38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

891 
val strip_tname = implode o tl o explode; 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

892 

38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

893 
fun pretty_list xs = Pretty.block (Pretty.str "[" :: 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

894 
flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @ 
13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

895 
[Pretty.str "]"]); 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

896 

38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

897 
fun mk_type p (TVar ((s, i), _)) = Pretty.str 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

898 
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T") 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

899 
 mk_type p (TFree (s, _)) = Pretty.str (strip_tname s ^ "T") 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

900 
 mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

901 
[Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","), 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

902 
Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]); 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

903 

17144  904 
fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str 
13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

905 
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F") 
17144  906 
 mk_term_of gr module p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F") 
907 
 mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I) 

16649  908 
(Pretty.block (separate (Pretty.brk 1) 
17144  909 
(Pretty.str (mk_qual_id module 
910 
(get_type_id' (fn s' => "term_of_" ^ s') s gr)) :: 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

911 
maps (fn T => 
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

912 
[mk_term_of gr module true T, mk_type true T]) Ts))); 
13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

913 

38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

914 

14105  915 
(**** Test data generators ****) 
916 

17144  917 
fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str 
14105  918 
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") 
17144  919 
 mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") 
25892
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

920 
 mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I) 
16649  921 
(Pretty.block (separate (Pretty.brk 1) 
17144  922 
(Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ 
20665  923 
(if member (op =) xs s then "'" else "")) :: 
25892
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

924 
(case tyc of 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

925 
("fun", [T, U]) => 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

926 
[mk_term_of gr module true T, mk_type true T, 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

927 
mk_gen gr module true xs a U, mk_type true U] 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

928 
 _ => maps (fn T => 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

929 
[mk_gen gr module true xs a T, mk_type true T]) Ts) @ 
20665  930 
(if member (op =) xs s then [Pretty.str a] else [])))); 
14105  931 

15531  932 
val test_fn : (int > (string * term) list option) ref = ref (fn _ => NONE); 
14105  933 

24456  934 
fun test_term thy quiet sz i t = 
14105  935 
let 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

936 
val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

937 
error "Term to be tested contains type variables"; 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

938 
val _ = null (term_vars t) orelse 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

939 
error "Term to be tested contains schematic variables"; 
14105  940 
val frees = map dest_Free (term_frees t); 
17549  941 
val frees' = frees ~~ 
942 
map (fn i => "arg" ^ string_of_int i) (1 upto length frees); 

17144  943 
val (code, gr) = setmp mode ["term_of", "test"] 
944 
(generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))]; 

24634  945 
val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^ 
17144  946 
space_implode "\n" (map snd code) ^ 
16649  947 
"\nopen Generated;\n\n" ^ Pretty.string_of 
14105  948 
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=", 
17549  949 
Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1, 
25892
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

950 
mk_let (map (fn ((s, T), s') => 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

951 
(mk_tuple [Pretty.str s', Pretty.str (s' ^ "_t")], 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

952 
Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1, 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

953 
Pretty.str "i"])) frees') 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

954 
(Pretty.block [Pretty.str "if ", 
17549  955 
mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'), 
15531  956 
Pretty.brk 1, Pretty.str "then NONE", 
14105  957 
Pretty.brk 1, Pretty.str "else ", 
15531  958 
Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" :: 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

959 
flat (separate [Pretty.str ",", Pretty.brk 1] 
17549  960 
(map (fn ((s, T), s') => [Pretty.block 
21056  961 
[Pretty.str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1, 
25892
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

962 
Pretty.str (s' ^ "_t ())")]]) frees')) @ 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

963 
[Pretty.str "]"])]]), 
3ff9d646a66a
Test data generation and conversion to terms are now more closely
berghofe
parents:
25400
diff
changeset

964 
Pretty.str ");"]) ^ 
17638  965 
"\n\nend;\n") (); 
24655
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

966 
val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy)); 
15531  967 
fun iter f k = if k > i then NONE 
14135
f8a25218b423
test_term now handles Match exception raised in generated code.
berghofe
parents:
14110
diff
changeset

968 
else (case (f () handle Match => 
24456  969 
(if quiet then () 
970 
else warning "Exception Match raised in generated code"; NONE)) of 

15531  971 
NONE => iter f (k+1)  SOME x => SOME x); 
972 
fun test k = if k > sz then NONE 

24456  973 
else (if quiet then () else priority ("Test data size: " ^ string_of_int k); 
14105  974 
case iter (fn () => !test_fn k) 1 of 
15531  975 
NONE => test (k+1)  SOME x => SOME x); 
17638  976 
in test 0 end; 
14105  977 

24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

978 
fun test_goal quiet ({size, iterations, default_type}, tvinsts) i assms state = 
14105  979 
let 
24456  980 
val thy = Proof.theory_of state; 
14105  981 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 
982 
 strip t = t; 

24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

983 
val (_, (_, st)) = Proof.get_goal state; 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

984 
val (gi, frees) = Logic.goal_params (prop_of st) i; 
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20286
diff
changeset

985 
val gi' = ObjectLogic.atomize_term thy (map_types 
24655
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

986 
(map_type_tfree (fn p as (s, S) => 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

987 
let val T = the_default (the_default (TFree p) default_type) 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

988 
(AList.lookup (op =) tvinsts s) 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

989 
in if Sign.of_sort thy (T, S) then T 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

990 
else error ("Type " ^ Sign.string_of_typ thy T ^ 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

991 
" to be substituted for variable " ^ 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

992 
Sign.string_of_typ thy (TFree p) ^ "\ndoes not have sort " ^ 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

993 
Sign.string_of_sort thy S) 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

994 
end)) 
24456  995 
(Logic.list_implies (assms, subst_bounds (frees, strip gi)))); 
24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

996 
in test_term thy quiet size iterations gi' end; 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

997 

08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

998 
fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found." 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

999 
 pretty_counterex ctxt (SOME cex) = 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1000 
Pretty.chunks (Pretty.str "Counterexample found:\n" :: 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1001 
map (fn (s, t) => 
24920  1002 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex); 
24456  1003 

25376
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1004 
val auto_quickcheck = ref false; 
24805
34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

1005 
val auto_quickcheck_time_limit = ref 5000; 
24456  1006 

1007 
fun test_goal' int state = 

24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1008 
let 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1009 
val ctxt = Proof.context_of state; 
25376
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1010 
val assms = map term_of (Assumption.assms_of ctxt); 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1011 
val params = get_test_params (Proof.theory_of state); 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1012 
fun test () = 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1013 
let 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1014 
val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit)) 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1015 
(try (test_goal true (params, []) 1 assms)) state; 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1016 
in 
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1017 
case res of 
25400  1018 
NONE => state 
1019 
 SOME NONE => state 

25376
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1020 
 SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "", 
25309  1021 
Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state 
25400  1022 
end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state); 
24456  1023 
in 
24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1024 
if int andalso !auto_quickcheck andalso not (!Toplevel.quiet) 
25376
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1025 
then test () 
24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1026 
else state 
24805
34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

1027 
end; 
24456  1028 

1029 
val _ = Context.add_setup 

1030 
(Context.theory_map (Specification.add_theorem_hook test_goal')); 

1031 

14105  1032 

17549  1033 
(**** Evaluator for terms ****) 
1034 

24655
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

1035 
val eval_result = ref (fn () => Bound 0); 
17549  1036 

25009
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1037 
fun eval_term thy t = 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1038 
let val e = PrintMode.setmp [] (fn () => 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1039 
let 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1040 
val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1041 
error "Term to be evaluated contains type variables"; 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1042 
val _ = (null (term_vars t) andalso null (term_frees t)) orelse 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1043 
error "Term to be evaluated contains variables"; 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1044 
val (code, gr) = setmp mode ["term_of"] 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1045 
(generate_code_i thy [] "Generated") 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1046 
[("result", Abs ("x", TFree ("'a", []), t))]; 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1047 
val s = "structure EvalTerm =\nstruct\n\n" ^ 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1048 
space_implode "\n" (map snd code) ^ 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1049 
"\nopen Generated;\n\n" ^ Pretty.string_of 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1050 
(Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>", 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1051 
Pretty.brk 1, 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1052 
mk_app false (mk_term_of gr "Generated" false (fastype_of t)) 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1053 
[Pretty.str "(result ())"], 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1054 
Pretty.str ");"]) ^ 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1055 
"\n\nend;\n"; 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1056 
val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy)) 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1057 
in !eval_result end) (); 
61946780de00
eval_term: moved actual evaluation out of CRITICAL section;
wenzelm
parents:
24920
diff
changeset

1058 
in e () end; 
17549  1059 

1060 
fun print_evaluated_term s = Toplevel.keep (fn state => 

1061 
let 

21506  1062 
val ctxt = Toplevel.context_of state; 
21002  1063 
val thy = ProofContext.theory_of ctxt; 
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24469
diff
changeset

1064 
val t = eval_term thy (Syntax.read_term ctxt s); 
17549  1065 
val T = Term.type_of t; 
1066 
in 

24585  1067 
Pretty.writeln 
24920  1068 
(Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk, 
1069 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)]) 

17549  1070 
end); 
1071 

20599  1072 
exception Evaluation of term; 
1073 

1074 
fun evaluation_oracle (thy, Evaluation t) = 

1075 
Logic.mk_equals (t, eval_term thy t); 

1076 

1077 
fun evaluation_conv ct = 

22596  1078 
let val {thy, t, ...} = rep_cterm ct 
24456  1079 
in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end; 
1080 

1081 
val _ = Context.add_setup 

1082 
(Theory.add_oracle ("evaluation", evaluation_oracle)); 

20599  1083 

17549  1084 

12452  1085 
(**** Interface ****) 
1086 

24634  1087 
val str = PrintMode.setmp [] Pretty.str; 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

1088 

11520  1089 
fun parse_mixfix rd s = 
1090 
(case Scan.finite Symbol.stopper (Scan.repeat 

1091 
( $$ "_" >> K Arg 

1092 
 $$ "?" >> K Ignore 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1093 
 $$ "\\<module>" >> K Module 
11520  1094 
 $$ "/"  Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length) 
1095 
 $$ "{"  $$ "*"  Scan.repeat1 

23784
75e6b9dd5336
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23655
diff
changeset

1096 
( $$ "'"  Scan.one Symbol.is_regular 
75e6b9dd5336
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23655
diff
changeset

1097 
 Scan.unless ($$ "*"  $$ "}") (Scan.one Symbol.is_regular))  
12452  1098 
$$ "*"  $$ "}" >> (Quote o rd o implode) 
11520  1099 
 Scan.repeat1 
23784
75e6b9dd5336
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23655
diff
changeset

1100 
( $$ "'"  Scan.one Symbol.is_regular 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1101 
 Scan.unless ($$ "_"  $$ "?"  $$ "\\<module>"  $$ "/"  $$ "{"  $$ "*") 
23784
75e6b9dd5336
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23655
diff
changeset

1102 
(Scan.one Symbol.is_regular)) >> (Pretty o str o implode))) 
11520  1103 
(Symbol.explode s) of 
1104 
(p, []) => p 

1105 
 _ => error ("Malformed annotation: " ^ quote s)); 

1106 

15801  1107 

17057  1108 
structure P = OuterParse and K = OuterKeyword; 
11520  1109 

24867  1110 
val _ = OuterSyntax.keywords ["attach", "file", "contains"]; 
1111 

17144  1112 
fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ") 
1113 
(snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n"; 

16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1114 

7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1115 
val parse_attach = Scan.repeat (P.$$$ "attach"  
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1116 
Scan.optional (P.$$$ "("  P.xname  P.$$$ ")") ""  
17144  1117 
(P.verbatim >> strip_whitespace)); 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1118 

24867  1119 
val _ = 
11520  1120 
OuterSyntax.command "types_code" 
11546  1121 
"associate types with target language types" K.thy_decl 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1122 
(Scan.repeat1 (P.xname  P.$$$ "("  P.string  P.$$$ ")"  parse_attach) >> 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

1123 
(fn xs => Toplevel.theory (fn thy => fold (assoc_type o 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

1124 
(fn ((name, mfx), aux) => (name, (parse_mixfix 
24707  1125 
(Syntax.read_typ_global thy) mfx, aux)))) xs thy))); 
11520  1126 

24867  1127 
val _ = 
11520  1128 
OuterSyntax.command "consts_code" 
11546  1129 
"associate constants with target language code" K.thy_decl 
11520  1130 
(Scan.repeat1 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

1131 
(P.term  
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1132 
P.$$$ "("  P.string  P.$$$ ")"  parse_attach) >> 
25376
87824cc5ff90
auto_quickcheck ref: set default in ProofGeneral/preferences only
wenzelm
parents:
25367
diff
changeset

1133 
(fn xs => Toplevel.theory (fn thy => fold (assoc_const o 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

1134 
(fn ((const, mfx), aux) => 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22846
diff
changeset

1135 
(const, (parse_mixfix (Sign.read_term thy) mfx, aux)))) xs thy))); 
11520  1136 

17144  1137 
fun parse_code lib = 
1138 
Scan.optional (P.$$$ "("  P.enum "," P.xname  P.$$$ ")") (!mode)  

1139 
(if lib then Scan.optional P.name "" else P.name)  

1140 
Scan.option (P.$$$ "file"  P.name)  

1141 
(if lib then Scan.succeed [] 

1142 
else Scan.optional (P.$$$ "imports"  Scan.repeat1 P.name) [])  

1143 
P.$$$ "contains"  

1144 
( Scan.repeat1 (P.name  P.$$$ "="  P.term) 

1145 
 Scan.repeat1 (P.term >> pair "")) >> 

1146 
(fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => 

1147 
let 

19299  1148 
val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); 
17144  1149 
val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs 
1150 
in ((case opt_fname of 

24655
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

1151 
NONE => ML_Context.use_mltext (space_implode "\n" (map snd code)) 
24b630fd008f
 eval_term no longer computes result during compile time
berghofe
parents:
24634
diff
changeset

1152 
false (SOME (Context.Theory thy)) 
17144  1153 
 SOME fname => 
1154 
if lib then 

1155 
app (fn (name, s) => File.write 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

1156 
(Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s) 
17144  1157 
(("ROOT", implode (map (fn (name, _) => 
1158 
"use \"" ^ name ^ ".ML\";\n") code)) :: code) 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21836
diff
changeset

1159 
else File.write (Path.explode fname) (snd (hd code))); 
17144  1160 
if lib then thy 
17412  1161 
else map_modules (Symtab.update (module, gr)) thy) 
17144  1162 
end)); 
1163 

24867  1164 
val _ = 
17144  1165 
OuterSyntax.command "code_library" 
1166 
"generates code for terms (one structure for each theory)" K.thy_decl 

1167 
(parse_code true); 

1168 

24867  1169 
val _ = 
17144  1170 
OuterSyntax.command "code_module" 
1171 
"generates code for terms (single structure, incremental)" K.thy_decl 

1172 
(parse_code false); 

11520  1173 

14105  1174 
val params = 
1175 
[("size", P.nat >> (K o set_size)), 

1176 
("iterations", P.nat >> (K o set_iterations)), 

1177 
("default_type", P.typ >> set_default_type)]; 

1178 

24022  1179 
val parse_test_params = P.short_ident : (fn s => 
1180 
P.$$$ "="  (AList.lookup (op =) params s > the_default Scan.fail)); 

14105  1181 

1182 
fun parse_tyinst xs = 

16458  1183 
(P.type_ident  P.$$$ "="  P.typ >> (fn (v, s) => fn thy => 
24707  1184 
fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs; 
14105  1185 

24867  1186 
val _ = 
14105  1187 
OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl 
1188 
(P.$$$ "["  P.list1 parse_test_params  P.$$$ "]" >> 

1189 
(fn fs => Toplevel.theory (fn thy => 

24456  1190 
map_test_params (Library.apply (map (fn f => f thy) fs)) thy))); 
14105  1191 

24867  1192 
val _ = 
14105  1193 
OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag 
1194 
(Scan.option (P.$$$ "["  P.list1 

16458  1195 
( parse_test_params >> (fn f => fn thy => apfst (f thy)) 
14105  1196 
 parse_tyinst)  P.$$$ "]")  Scan.optional P.nat 1 >> 
24565
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1197 
(fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st > 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1198 
test_goal false (Library.apply (the_default [] 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1199 
(Option.map (map (fn f => f (Toplevel.theory_of st))) ps)) 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1200 
(get_test_params (Toplevel.theory_of st), [])) g [] > 
08578e380a41
Auto quickcheck now displays counterexample using Proof.goal_message
berghofe
parents:
24508
diff
changeset

1201 
pretty_counterex (Toplevel.context_of st) > Pretty.writeln))); 
14105  1202 

24867  1203 
val _ = 
17549  1204 
OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag 
1205 
(P.term >> (Toplevel.no_timing oo print_evaluated_term)); 

1206 

11520  1207 
end; 
24805
34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

1208 

34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

1209 
val auto_quickcheck = Codegen.auto_quickcheck; 
34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

1210 
val auto_quickcheck_time_limit = Codegen.auto_quickcheck_time_limit; 
34cbfb87dfe8
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
wenzelm
parents:
24707
diff
changeset

1211 