author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18788  4f4ed2a01152 
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 

18728  29 
val add_attribute: string > (Args.T list > attribute * Args.T list) > theory > theory 
15261  30 
val add_preprocessor: (theory > thm list > thm list) > theory > theory 
31 
val preprocess: theory > thm list > thm list 

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

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

37 
(string * string) list * codegr 

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

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

39 
(string * string) list)) list > theory > theory 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

40 
val assoc_consts_i: (xstring * typ option * (term mixfix list * 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

41 
(string * string) list)) list > theory > theory 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

42 
val assoc_types: (xstring * (typ mixfix list * 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

43 
(string * string) list)) list > theory > theory 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

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

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

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

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

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

52 
codegr * typ > codegr * Pretty.T 

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

56 
val get_const_id: string > codegr > string * string 

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

58 
val get_type_id: string > codegr > string * string 

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

61 
val rename_terms: term list > term list 

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

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

11520  68 
val is_instance: theory > typ > typ > bool 
69 
val parens: Pretty.T > Pretty.T 

70 
val mk_app: bool > Pretty.T > Pretty.T list > Pretty.T 

71 
val eta_expand: term > term list > int > term 

14105  72 
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

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

14105  76 
val test_fn: (int > (string * term) list option) ref 
77 
val test_term: theory > int > int > term > (string * term) list option 

17549  78 
val eval_result: term ref 
79 
val eval_term: theory > term > term 

12452  80 
val parse_mixfix: (string > 'a) > string > 'a mixfix list 
18102  81 
val quotes_of: 'a mixfix list > 'a list 
18281  82 
val num_args_of: 'a mixfix list > int 
18102  83 
val replace_quotes: 'b list > 'a mixfix list > 'b mixfix list 
18702  84 
val fillin_mixfix: ('a > Pretty.T) > 'a mixfix list > 'a list > Pretty.T 
16649  85 
val mk_deftab: theory > deftab 
17549  86 

17144  87 
val get_node: codegr > string > node 
88 
val add_edge: string * string > codegr > codegr 

89 
val add_edge_acyclic: string * string > codegr > codegr 

90 
val del_nodes: string list > codegr > codegr 

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

92 
val new_node: string * node > codegr > codegr 

11520  93 
end; 
94 

95 
structure Codegen : CODEGEN = 

96 
struct 

97 

98 
val quiet_mode = ref true; 

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

100 

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

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

102 

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

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

104 

11520  105 
(**** Mixfix syntax ****) 
106 

12452  107 
datatype 'a mixfix = 
11520  108 
Arg 
109 
 Ignore 

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

110 
 Module 
11520  111 
 Pretty of Pretty.T 
12452  112 
 Quote of 'a; 
11520  113 

114 
fun is_arg Arg = true 

115 
 is_arg Ignore = true 

116 
 is_arg _ = false; 

117 

12452  118 
fun quotes_of [] = [] 
119 
 quotes_of (Quote q :: ms) = q :: quotes_of ms 

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

121 

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

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

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

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

11520  126 

18281  127 
fun num_args_of x = length (List.filter is_arg x); 
11520  128 

129 

130 
(**** theory data ****) 

131 

16649  132 
(* preprocessed definition table *) 
133 

134 
type deftab = 

135 
(typ * (* type of constant *) 

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

137 
(term list * (* parameters *) 

138 
term))) (* righthand side *) 

139 
list Symtab.table; 

140 

141 
(* code dependency graph *) 

142 

17144  143 
type nametab = (string * string) Symtab.table * unit Symtab.table; 
144 

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

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

147 

148 
type node = 

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

17144  151 
string); (* piece of code *) 
152 

153 
type codegr = 

154 
node Graph.T * 

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

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

157 

158 
val emptygr : codegr = (Graph.empty, 

159 
((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty))); 

16649  160 

14105  161 
(* type of code generators *) 
11520  162 

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

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

166 
codegr > (* code dependency graph *) 

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

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

171 
(codegr * Pretty.T) option; 

12452  172 

14105  173 
(* parameters for random testing *) 
174 

175 
type test_params = 

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

177 

178 
fun merge_test_params 

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

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

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

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

183 
default_type = case default_type1 of 

15531  184 
NONE => default_type2 
14105  185 
 _ => default_type1}; 
186 

187 
val default_test_params : test_params = 

15531  188 
{size = 10, iterations = 100, default_type = NONE}; 
14105  189 

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

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

192 

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

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

195 

16458  196 
fun set_default_type s thy ({size, iterations, ...} : test_params) = 
14105  197 
{size = size, iterations = iterations, 
16458  198 
default_type = SOME (typ_of (read_ctyp thy s))}; 
14105  199 

200 
(* data kind 'Pure/codegen' *) 

16458  201 

202 
structure CodegenData = TheoryDataFun 

203 
(struct 

11520  204 
val name = "Pure/codegen"; 
205 
type T = 

12452  206 
{codegens : (string * term codegen) list, 
207 
tycodegens : (string * typ codegen) list, 

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

208 
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

209 
types : (string * (typ mixfix list * (string * string) list)) list, 
18728  210 
attrs: (string * (Args.T list > attribute * Args.T list)) list, 
15261  211 
preprocs: (stamp * (theory > thm list > thm list)) list, 
17144  212 
modules: codegr Symtab.table, 
14105  213 
test_params: test_params}; 
11520  214 

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

215 
val empty = 
14105  216 
{codegens = [], tycodegens = [], consts = [], types = [], attrs = [], 
17144  217 
preprocs = [], modules = Symtab.empty, test_params = default_test_params}; 
11520  218 
val copy = I; 
16458  219 
val extend = I; 
11520  220 

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

222 
({codegens = codegens1, tycodegens = tycodegens1, 
14105  223 
consts = consts1, types = types1, attrs = attrs1, 
17144  224 
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

225 
{codegens = codegens2, tycodegens = tycodegens2, 
14105  226 
consts = consts2, types = types2, attrs = attrs2, 
17144  227 
preprocs = preprocs2, modules = modules2, test_params = test_params2}) = 
15261  228 
{codegens = merge_alists' codegens1 codegens2, 
229 
tycodegens = merge_alists' tycodegens1 tycodegens2, 

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

230 
consts = merge_alists consts1 consts2, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

231 
types = merge_alists types1 types2, 
14105  232 
attrs = merge_alists attrs1 attrs2, 
15261  233 
preprocs = merge_alists' preprocs1 preprocs2, 
17144  234 
modules = Symtab.merge (K true) (modules1, modules2), 
14105  235 
test_params = merge_test_params test_params1 test_params2}; 
11520  236 

16458  237 
fun print _ ({codegens, tycodegens, ...} : T) = 
12452  238 
Pretty.writeln (Pretty.chunks 
239 
[Pretty.strs ("term code generators:" :: map fst codegens), 

240 
Pretty.strs ("type code generators:" :: map fst tycodegens)]); 

16458  241 
end); 
11520  242 

18708  243 
val _ = Context.add_setup CodegenData.init; 
11520  244 
val print_codegens = CodegenData.print; 
245 

246 

14105  247 
(**** access parameters for random testing ****) 
248 

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

250 

251 
fun map_test_params f thy = 

17144  252 
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = 
14105  253 
CodegenData.get thy; 
254 
in CodegenData.put {codegens = codegens, tycodegens = tycodegens, 

15261  255 
consts = consts, types = types, attrs = attrs, preprocs = preprocs, 
17144  256 
modules = modules, test_params = f test_params} thy 
257 
end; 

258 

259 

260 
(**** access modules ****) 

261 

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

263 

264 
fun map_modules f thy = 

265 
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = 

266 
CodegenData.get thy; 

267 
in CodegenData.put {codegens = codegens, tycodegens = tycodegens, 

268 
consts = consts, types = types, attrs = attrs, preprocs = preprocs, 

269 
modules = f modules, test_params = test_params} thy 

14105  270 
end; 
271 

272 

12452  273 
(**** add new code generators to theory ****) 
11520  274 

275 
fun add_codegen name f thy = 

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

280 
tycodegens = tycodegens, consts = consts, types = types, 
17144  281 
attrs = attrs, preprocs = preprocs, modules = modules, 
282 
test_params = test_params} thy 

15531  283 
 SOME _ => error ("Code generator " ^ name ^ " already declared")) 
12452  284 
end; 
285 

286 
fun add_tycodegen name f thy = 

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

291 
codegens = codegens, consts = consts, types = types, 
17144  292 
attrs = attrs, preprocs = preprocs, modules = modules, 
293 
test_params = test_params} thy 

15531  294 
 SOME _ => error ("Code generator " ^ name ^ " already declared")) 
11520  295 
end; 
296 

297 

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

298 
(**** code attribute ****) 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

299 

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

300 
fun add_attribute name att thy = 
17144  301 
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = 
14105  302 
CodegenData.get thy 
17521  303 
in (case AList.lookup (op =) attrs name of 
15531  304 
NONE => CodegenData.put {tycodegens = tycodegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

305 
codegens = codegens, consts = consts, types = types, 
15261  306 
attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs, 
17144  307 
preprocs = preprocs, modules = modules, 
15261  308 
test_params = test_params} thy 
15531  309 
 SOME _ => error ("Code attribute " ^ name ^ " already declared")) 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

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

311 

14197  312 
fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a)  p; 
313 

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

314 
val code_attr = 
18728  315 
Attrib.syntax (Scan.peek (fn context => foldr op  Scan.fail (map mk_parser 
316 
(#attrs (CodegenData.get (Context.theory_of context)))))); 

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

317 

15801  318 
val _ = Context.add_setup 
18728  319 
(Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]); 
15801  320 

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

321 

15261  322 
(**** preprocessors ****) 
323 

324 
fun add_preprocessor p thy = 

17144  325 
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = 
15261  326 
CodegenData.get thy 
327 
in CodegenData.put {tycodegens = tycodegens, 

328 
codegens = codegens, consts = consts, types = types, 

329 
attrs = attrs, preprocs = (stamp (), p) :: preprocs, 

17144  330 
modules = modules, test_params = test_params} thy 
15261  331 
end; 
332 

333 
fun preprocess thy ths = 

334 
let val {preprocs, ...} = CodegenData.get thy 

15570  335 
in Library.foldl (fn (ths, (_, f)) => f thy ths) (ths, preprocs) end; 
15261  336 

17549  337 
fun preprocess_term thy t = 
338 
let 

339 
val x = Free (variant (add_term_names (t, [])) "x", fastype_of t); 

340 
(* fake definition *) 

341 
val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) 

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

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

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

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

346 
 _ => err () 

347 
end; 

18281  348 

18728  349 
val unfold_attr = Thm.declaration_attribute (fn eqn => Context.map_theory 
15261  350 
let 
18728  351 
val names = term_consts (fst (Logic.dest_equals (prop_of eqn))); 
15261  352 
fun prep thy = map (fn th => 
17666  353 
let val prop = prop_of th 
354 
in 

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

356 
then rewrite_rule [eqn] (Thm.transfer thy th) 

357 
else th 

358 
end) 

18728  359 
in add_preprocessor prep end); 
15261  360 

18708  361 
val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr)); 
15801  362 

15261  363 

11520  364 
(**** associate constants with target language code ****) 
365 

15570  366 
fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) => 
11520  367 
let 
17144  368 
val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = 
14105  369 
CodegenData.get thy; 
16458  370 
val cname = Sign.intern_const thy s; 
11520  371 
in 
16458  372 
(case Sign.const_type thy cname of 
15531  373 
SOME T => 
11520  374 
let val T' = (case tyopt of 
15531  375 
NONE => T 
376 
 SOME ty => 

16458  377 
let val U = prep_type thy ty 
378 
in if Sign.typ_instance thy (U, T) then U 

11520  379 
else error ("Illegal type constraint for constant " ^ cname) 
380 
end) 

18320
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

381 
in 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

382 
if num_args_of (fst syn) > length (binder_types T') then 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

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

384 
else (case AList.lookup (op =) consts (cname, T') of 
15531  385 
NONE => CodegenData.put {codegens = codegens, 
12452  386 
tycodegens = tycodegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

387 
consts = ((cname, T'), syn) :: consts, 
15261  388 
types = types, attrs = attrs, preprocs = preprocs, 
17144  389 
modules = modules, test_params = test_params} thy 
15531  390 
 SOME _ => error ("Constant " ^ cname ^ " already associated with code")) 
11520  391 
end 
392 
 _ => error ("Not a constant: " ^ s)) 

393 
end) (thy, xs); 

394 

395 
val assoc_consts_i = gen_assoc_consts (K I); 

16458  396 
val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp); 
11520  397 

15801  398 

11520  399 
(**** associate types with target language types ****) 
400 

15570  401 
fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) => 
11520  402 
let 
17144  403 
val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = 
14105  404 
CodegenData.get thy; 
16649  405 
val tc = Sign.intern_type thy s 
11520  406 
in 
18320
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

407 
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

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

409 
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

410 
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

411 
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

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

413 
tycodegens = tycodegens, consts = consts, 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

414 
types = (tc, syn) :: types, attrs = attrs, 
ce523820ff75
assoc_consts and assoc_types now check number of arguments in template.
berghofe
parents:
18281
diff
changeset

415 
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

416 
 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

417 
 _ => error ("Not a type constructor: " ^ s) 
11520  418 
end) (thy, xs); 
419 

17521  420 
fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s; 
11546  421 

11520  422 

423 
(**** make valid ML identifiers ****) 

424 

14858  425 
fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse 
426 
Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x; 

427 

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

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

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

431 
 _ => sys_error "dest_sym"); 

16458  432 

14858  433 
fun mk_id s = if s = "" then "" else 
11520  434 
let 
14858  435 
fun check_str [] = [] 
436 
 check_str xs = (case take_prefix is_ascii_letdig xs of 

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

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

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

440 
else (case dest_sym z of 

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

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

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

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

445 
val s' = space_implode "_" 

15570  446 
(List.concat (map (check_str o Symbol.explode) (NameSpace.unpack s))) 
11520  447 
in 
14858  448 
if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' 
11520  449 
end; 
450 

17144  451 
fun mk_long_id (p as (tab, used)) module s = 
16649  452 
let 
17144  453 
fun find_name [] = sys_error "mk_long_id" 
454 
 find_name (ys :: yss) = 

455 
let 

456 
val s' = NameSpace.pack ys 

457 
val s'' = NameSpace.append module s' 

17412  458 
in case Symtab.lookup used s'' of 
17261  459 
NONE => ((module, s'), 
17412  460 
(Symtab.update_new (s, (module, s')) tab, 
461 
Symtab.update_new (s'', ()) used)) 

17144  462 
 SOME _ => find_name yss 
463 
end 

17412  464 
in case Symtab.lookup tab s of 
17144  465 
NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) 
466 
 SOME name => (name, p) 

16649  467 
end; 
468 

17144  469 
(* module: module name for caller *) 
470 
(* module': module name for callee *) 

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

16649  472 

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

475 

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

16649  477 
let 
17144  478 
val ((module, s), tab1') = mk_long_id tab1 module cname 
479 
val s' = mk_id s; 

16649  480 
val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' 
17144  481 
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

482 

17144  483 
fun get_const_id cname (gr, (tab1, tab2)) = 
17412  484 
case Symtab.lookup (fst tab1) cname of 
17144  485 
NONE => error ("get_const_id: no such constant: " ^ quote cname) 
486 
 SOME (module, s) => 

487 
let 

488 
val s' = mk_id s; 

489 
val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' 

490 
in (module, s'') end; 

491 

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

16649  493 
let 
17144  494 
val ((module, s), tab2') = mk_long_id tab2 module tyname 
495 
val s' = mk_id s; 

496 
val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' 

497 
in ((gr, (tab1, tab2')), (module, s'')) end; 

16649  498 

17144  499 
fun get_type_id tyname (gr, (tab1, tab2)) = 
17412  500 
case Symtab.lookup (fst tab2) tyname of 
17144  501 
NONE => error ("get_type_id: no such type: " ^ quote tyname) 
502 
 SOME (module, s) => 

503 
let 

504 
val s' = mk_id s; 

505 
val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' 

506 
in (module, s'') end; 

507 

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

509 

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

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

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

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

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

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

16649  516 

18281  517 
fun theory_of_type s thy = 
16649  518 
if Sign.declared_tyname thy s 
519 
then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy) 

520 
else NONE; 

521 

18281  522 
fun theory_of_const s thy = 
16649  523 
if Sign.declared_const thy s 
524 
then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy) 

525 
else NONE; 

526 

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

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

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

530 

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

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

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

11520  534 

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

535 
fun rename_terms ts = 
11520  536 
let 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

537 
val names = foldr add_term_names 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

538 
(map (fst o fst) (Drule.vars_of_terms ts)) ts; 
14858  539 
val reserved = names inter ThmDatabase.ml_reserved; 
15570  540 
val (illegal, alt_names) = split_list (List.mapPartial (fn s => 
15531  541 
let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names) 
14858  542 
val ps = (reserved @ illegal) ~~ 
543 
variantlist (map (suffix "'") reserved @ alt_names, names); 

11520  544 

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

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

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

11520  549 
 rename (Abs (s, T, t)) = Abs (s, T, rename t) 
550 
 rename (t $ u) = rename t $ rename u 

551 
 rename t = t; 

552 
in 

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

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

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

555 

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

556 
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

557 

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

558 

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

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

560 

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

561 
fun is_instance thy T1 T2 = 
16649  562 
Sign.typ_instance thy (T1, Type.varifyT T2); 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

563 

18098  564 
fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

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

566 

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

567 
fun get_aux_code xs = List.mapPartial (fn (m, code) => 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

568 
if m = "" orelse m mem !mode then SOME code else NONE) xs; 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

569 

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

571 
let 
16649  572 
val axmss = map (fn thy' => 
573 
(Context.theory_name thy', snd (#axioms (Theory.rep_theory thy')))) 

574 
(thy :: Theory.ancestors_of thy); 

15261  575 
fun prep_def def = (case preprocess thy [def] of 
16649  576 
[def'] => prop_of def'  _ => error "mk_deftab: bad preprocessor"); 
15261  577 
fun dest t = 
578 
let 

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

580 
val (c, args) = strip_comb lhs; 

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

15531  583 
end handle TERM _ => NONE; 
16649  584 
fun add_def thyname (defs, (name, t)) = (case dest t of 
585 
NONE => defs 

586 
 SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of 

587 
NONE => defs 

17412  588 
 SOME (s, (T, (args, rhs))) => Symtab.update 
17261  589 
(s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) :: 
17412  590 
if_none (Symtab.lookup defs s) []) defs)) 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

591 
in 
16649  592 
foldl (fn ((thyname, axms), defs) => 
593 
Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss 

11520  594 
end; 
595 

17412  596 
fun get_defn thy defs s T = (case Symtab.lookup defs s of 
16649  597 
NONE => NONE 
598 
 SOME ds => 

599 
let val i = find_index (is_instance thy T o fst) ds 

600 
in if i >= 0 then 

601 
SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) 

602 
else NONE 

603 
end); 

604 

11520  605 

12452  606 
(**** invoke suitable code generator for term / type ****) 
11520  607 

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

610 

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

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

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

614 
Sign.string_of_term thy t) 

15531  615 
 SOME x => x); 
12452  616 

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

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

620 
Sign.string_of_typ thy T) 

15531  621 
 SOME x => x); 
11520  622 

623 

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

625 

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

627 

628 
fun pretty_fn [] p = [p] 

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

630 
Pretty.brk 1 :: pretty_fn xs p; 

631 

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

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

633 
 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

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

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

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

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

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

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

641 
 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

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

643 
 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

644 
q :: pretty_mixfix module module' ms ps qs; 
11520  645 

18102  646 
fun replace_quotes [] [] = [] 
647 
 replace_quotes xs (Arg :: ms) = 

648 
Arg :: replace_quotes xs ms 

649 
 replace_quotes xs (Ignore :: ms) = 

650 
Ignore :: replace_quotes xs ms 

651 
 replace_quotes xs (Module :: ms) = 

652 
Module :: replace_quotes xs ms 

653 
 replace_quotes xs (Pretty p :: ms) = 

654 
Pretty p :: replace_quotes xs ms 

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

656 
Quote x :: replace_quotes xs ms; 

657 

18702  658 
fun fillin_mixfix f ms args = 
18098  659 
let 
18281  660 
fun fillin [] [] = 
661 
[] 

662 
 fillin (Arg :: ms) (a :: args) = 

18702  663 
f a :: fillin ms args 
18281  664 
 fillin (Ignore :: ms) args = 
665 
fillin ms args 

666 
 fillin (Module :: ms) args = 

667 
fillin ms args 

668 
 fillin (Pretty p :: ms) args = 

669 
p :: fillin ms args 

670 
 fillin (Quote q :: ms) args = 

18702  671 
f q :: fillin ms args 
18281  672 
in Pretty.block (fillin ms args) end; 
18098  673 

11520  674 

12452  675 
(**** default code generators ****) 
11520  676 

677 
fun eta_expand t ts i = 

678 
let 

679 
val (Ts, _) = strip_type (fastype_of t); 

680 
val j = i  length ts 

681 
in 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

682 
foldr (fn (T, t) => Abs ("x", T, t)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

683 
(list_comb (t, ts @ map Bound (j1 downto 0))) (Library.take (j, Ts)) 
11520  684 
end; 
685 

686 
fun mk_app _ p [] = p 

687 
 mk_app brack p ps = if brack then 

688 
Pretty.block (Pretty.str "(" :: 

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

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

691 

14858  692 
fun new_names t xs = variantlist (map mk_id xs, 
11520  693 
map (fst o fst o dest_Var) (term_vars t) union 
694 
add_term_names (t, ThmDatabase.ml_reserved)); 

695 

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

697 

17144  698 
fun if_library x y = if "library" mem !mode then x else y; 
699 

700 
fun default_codegen thy defs gr dep module brack t = 

11520  701 
let 
702 
val (u, ts) = strip_comb t; 

17144  703 
fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) 
11520  704 
in (case u of 
14105  705 
Var ((s, i), T) => 
706 
let 

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

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

712 

14105  713 
 Free (s, T) => 
714 
let 

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

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

719 
 Const (s, T) => 

720 
(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

721 
SOME (ms, aux) => 
18281  722 
let val i = num_args_of ms 
11520  723 
in if length ts < i then 
17144  724 
default_codegen thy defs gr dep module brack (eta_expand u ts i) 
11520  725 
else 
726 
let 

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

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

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

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

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

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

736 
(if_library module' module, "") 

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

738 
(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

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

17549  742 
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

743 
NONE => (case get_aux_code aux of 
17549  744 
[] => (gr4, p module) 
17144  745 
 xs => (add_edge (node_id, dep) (new_node 
17549  746 
(node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4), 
17144  747 
p module')) 
748 
 SOME (_, module'', _) => 

17549  749 
(add_edge (node_id, dep) gr4, p module'')) 
11520  750 
end 
751 
end 

16649  752 
 NONE => (case get_defn thy defs s T of 
15531  753 
NONE => NONE 
17144  754 
 SOME ((U, (thyname, (args, rhs))), k) => 
11520  755 
let 
17144  756 
val module' = if_library thyname module; 
757 
val suffix = (case k of NONE => ""  SOME i => " def" ^ string_of_int i); 

16649  758 
val node_id = s ^ suffix; 
17144  759 
val (gr', (ps, def_id)) = codegens true (gr, ts) >>> 
760 
mk_const_id module' (s ^ suffix); 

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

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

763 
NONE => 

764 
let 

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

766 
val (Ts, _) = strip_type T; 

767 
val (args', rhs') = 

768 
if not (null args) orelse null Ts then (args, rhs) else 

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

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

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

772 
(add_edge (node_id, dep) 

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

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

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

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

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

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

779 
(if null args' then 

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

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

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

783 
p) 

784 
end 

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

11520  786 
end)) 
787 

788 
 Abs _ => 

789 
let 

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

791 
val t = strip_abs_body u 

792 
val bs' = new_names t bs; 

12452  793 
val (gr1, ps) = codegens true (gr, ts); 
17144  794 
val (gr2, p) = invoke_codegen thy defs dep module false 
12452  795 
(gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); 
11520  796 
in 
15531  797 
SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ 
11520  798 
[Pretty.str ")"])) ps) 
799 
end 

800 

15531  801 
 _ => NONE) 
11520  802 
end; 
803 

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

811 
 SOME (ms, aux) => 
12452  812 
let 
813 
val (gr', ps) = foldl_map 

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

818 
(gr', quotes_of ms); 
17144  819 
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

820 
val node_id = s ^ " (type)"; 
17144  821 
fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) 
822 
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

823 
NONE => (case get_aux_code aux of 
17144  824 
[] => (gr'', p module') 
825 
 xs => (fst (mk_type_id module' s 

826 
(add_edge (node_id, dep) (new_node (node_id, 

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

828 
p module')) 

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

830 
(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

831 
end); 
12452  832 

15801  833 
val _ = Context.add_setup 
18708  834 
(add_codegen "default" default_codegen #> 
835 
add_tycodegen "default" default_tycodegen); 

15801  836 

11520  837 

16649  838 
fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n"; 
839 

17521  840 
fun add_to_module name s = AList.map_entry (op =) name (suffix s); 
16649  841 

17144  842 
fun output_code gr module xs = 
16649  843 
let 
17144  844 
val code = List.mapPartial (fn s => 
845 
let val c as (_, module', _) = Graph.get_node gr s 

846 
in if module = "" orelse module = module' then SOME (s, c) else NONE end) 

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

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

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

18098  851 
(Library.find_first (equal b o #2 o Graph.get_node gr) 
16649  852 
(Graph.imm_succs gr x)) 
853 
else NONE) code 

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

855 
 string_of_cycle _ = "" 

856 
in 

17144  857 
if module = "" then 
16649  858 
let 
859 
val modules = distinct (map (#2 o snd) code); 

860 
val mod_gr = foldr (uncurry Graph.add_edge_acyclic) 

861 
(foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules) 

17144  862 
(List.concat (map (fn (s, (_, module, _)) => map (pair module) 
863 
(filter_out (equal module) (map (#2 o Graph.get_node gr) 

16649  864 
(Graph.imm_succs gr s)))) code)); 
865 
val modules' = 

866 
rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) 

867 
in 

17144  868 
foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms) 
16649  869 
(map (rpair "") modules') code 
870 
end handle Graph.CYCLES (cs :: _) => 

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

872 
"\n" ^ string_of_cycle cs) 

17144  873 
else [(module, implode (map (#3 o snd) code))] 
16649  874 
end; 
11520  875 

17144  876 
fun gen_generate_code prep_term thy modules module = 
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14197
diff
changeset

877 
setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => 
11520  878 
let 
17144  879 
val _ = assert (module <> "" orelse 
880 
"library" mem !mode andalso forall (equal "" o fst) xs) 

881 
"missing module name"; 

882 
val graphs = get_modules thy; 

16649  883 
val defs = mk_deftab thy; 
17144  884 
val gr = new_node ("<Top>", (NONE, module, "")) 
885 
(foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => 

886 
(Graph.merge (fn ((_, module, _), (_, module', _)) => 

887 
module = module') (gr, gr'), 

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

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

892 
handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); 

16649  893 
fun expand (t as Abs _) = t 
894 
 expand t = (case fastype_of t of 

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

11520  896 
val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) 
17144  897 
(invoke_codegen thy defs "<Top>" module false (gr, t))) 
17549  898 
(gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs); 
17144  899 
val code = List.mapPartial 
900 
(fn ("", _) => NONE 

901 
 (s', p) => SOME (Pretty.string_of (Pretty.block 

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

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

904 
val code'' = 

905 
List.mapPartial (fn (name, s) => 

906 
if "library" mem !mode andalso name = module andalso null code 

907 
then NONE 

908 
else SOME (name, mk_struct name s)) 

909 
((if null code then I 

910 
else add_to_module module code') 

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

16649  912 
in 
17144  913 
(code'', del_nodes ["<Top>"] gr') 
16649  914 
end)); 
11520  915 

916 
val generate_code_i = gen_generate_code (K I); 

917 
val generate_code = gen_generate_code 

16458  918 
(fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT); 
11520  919 

12452  920 

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

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

922 

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

923 
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

924 

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

925 
fun pretty_list xs = Pretty.block (Pretty.str "[" :: 
15570  926 
List.concat (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

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

928 

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

929 
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

930 
(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

931 
 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

932 
 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

933 
[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

934 
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

935 

17144  936 
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

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

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

16649  943 
List.concat (map (fn T => 
17144  944 
[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

945 

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

946 

14105  947 
(**** Test data generators ****) 
948 

17144  949 
fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str 
14105  950 
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") 
17144  951 
 mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") 
952 
 mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I) 

16649  953 
(Pretty.block (separate (Pretty.brk 1) 
17144  954 
(Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ 
16649  955 
(if s mem xs then "'" else "")) :: 
17144  956 
map (mk_gen gr module true xs a) Ts @ 
16649  957 
(if s mem xs then [Pretty.str a] else [])))); 
14105  958 

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

17638  961 
fun test_term thy sz i t = 
14105  962 
let 
963 
val _ = assert (null (term_tvars t) andalso null (term_tfrees t)) 

964 
"Term to be tested contains type variables"; 

965 
val _ = assert (null (term_vars t)) 

966 
"Term to be tested contains schematic variables"; 

967 
val frees = map dest_Free (term_frees t); 

17549  968 
val frees' = frees ~~ 
969 
map (fn i => "arg" ^ string_of_int i) (1 upto length frees); 

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

17638  972 
val s = setmp print_mode [] (fn () => "structure TestTerm =\nstruct\n\n" ^ 
17144  973 
space_implode "\n" (map snd code) ^ 
16649  974 
"\nopen Generated;\n\n" ^ Pretty.string_of 
14105  975 
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=", 
17549  976 
Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1, 
14105  977 
Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, 
17549  978 
Pretty.blk (0, separate Pretty.fbrk (map (fn ((s, T), s') => 
979 
Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, 

17144  980 
mk_gen gr "Generated" false [] "" T, Pretty.brk 1, 
17549  981 
Pretty.str "i;"]) frees')), 
14105  982 
Pretty.brk 1, Pretty.str "in", Pretty.brk 1, 
983 
Pretty.block [Pretty.str "if ", 

17549  984 
mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'), 
15531  985 
Pretty.brk 1, Pretty.str "then NONE", 
14105  986 
Pretty.brk 1, Pretty.str "else ", 
15531  987 
Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" :: 
15570  988 
List.concat (separate [Pretty.str ",", Pretty.brk 1] 
17549  989 
(map (fn ((s, T), s') => [Pretty.block 
15326
ff21cddee442
Made test_term escape special characters in strings that caused the
berghofe
parents:
15261
diff
changeset

990 
[Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1, 
17144  991 
mk_app false (mk_term_of gr "Generated" false T) 
17549  992 
[Pretty.str s'], Pretty.str ")"]]) frees')) @ 
14105  993 
[Pretty.str "]"])]], 
14980  994 
Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ 
17638  995 
"\n\nend;\n") (); 
14105  996 
val _ = use_text Context.ml_output false s; 
15531  997 
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

998 
else (case (f () handle Match => 
15531  999 
(warning "Exception Match raised in generated code"; NONE)) of 
1000 
NONE => iter f (k+1)  SOME x => SOME x); 

1001 
fun test k = if k > sz then NONE 

14105  1002 
else (priority ("Test data size: " ^ string_of_int k); 
1003 
case iter (fn () => !test_fn k) 1 of 

15531  1004 
NONE => test (k+1)  SOME x => SOME x); 
17638  1005 
in test 0 end; 
14105  1006 

1007 
fun test_goal ({size, iterations, default_type}, tvinsts) i st = 

1008 
let 

16458  1009 
val thy = Toplevel.theory_of st; 
14105  1010 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 
1011 
 strip t = t; 

1012 
val (gi, frees) = Logic.goal_params 

1013 
(prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i; 

16458  1014 
val gi' = ObjectLogic.atomize_term thy (map_term_types 
17521  1015 
(map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s, 
1016 
getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi))); 

14105  1017 
in case test_term (Toplevel.theory_of st) size iterations gi' of 
15531  1018 
NONE => writeln "No counterexamples found." 
1019 
 SOME cex => writeln ("Counterexample found:\n" ^ 

14105  1020 
Pretty.string_of (Pretty.chunks (map (fn (s, t) => 
1021 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, 

16458  1022 
Sign.pretty_term thy t]) cex))) 
14105  1023 
end; 
1024 

1025 

17549  1026 
(**** Evaluator for terms ****) 
1027 

1028 
val eval_result = ref (Bound 0); 

1029 

1030 
fun eval_term thy = setmp print_mode [] (fn t => 

1031 
let 

1032 
val _ = assert (null (term_tvars t) andalso null (term_tfrees t)) 

1033 
"Term to be evaluated contains type variables"; 

1034 
val _ = assert (null (term_vars t) andalso null (term_frees t)) 

1035 
"Term to be evaluated contains variables"; 

1036 
val (code, gr) = setmp mode ["term_of"] 

1037 
(generate_code_i thy [] "Generated") [("result", t)]; 

1038 
val s = "structure EvalTerm =\nstruct\n\n" ^ 

1039 
space_implode "\n" (map snd code) ^ 

1040 
"\nopen Generated;\n\n" ^ Pretty.string_of 

1041 
(Pretty.block [Pretty.str "val () = Codegen.eval_result :=", 

1042 
Pretty.brk 1, 

1043 
mk_app false (mk_term_of gr "Generated" false (fastype_of t)) 

1044 
[Pretty.str "result"], 

1045 
Pretty.str ";"]) ^ 

1046 
"\n\nend;\n"; 

1047 
val _ = use_text Context.ml_output false s 

1048 
in !eval_result end); 

1049 

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

1051 
let 

1052 
val state' = Toplevel.enter_forward_proof state; 

1053 
val ctxt = Proof.context_of state'; 

1054 
val t = eval_term (Proof.theory_of state') (ProofContext.read_term ctxt s); 

1055 
val T = Term.type_of t; 

1056 
in 

1057 
writeln (Pretty.string_of 

1058 
(Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk, 

1059 
Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])) 

1060 
end); 

1061 

1062 

12452  1063 
(**** Interface ****) 
1064 

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

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

1066 

11520  1067 
fun parse_mixfix rd s = 
1068 
(case Scan.finite Symbol.stopper (Scan.repeat 

1069 
( $$ "_" >> K Arg 

1070 
 $$ "?" >> K Ignore 

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

1071 
 $$ "\\<module>" >> K Module 
11520  1072 
 $$ "/"  Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length) 
1073 
 $$ "{"  $$ "*"  Scan.repeat1 

1074 
( $$ "'"  Scan.one Symbol.not_eof 

1075 
 Scan.unless ($$ "*"  $$ "}") (Scan.one Symbol.not_eof))  

12452  1076 
$$ "*"  $$ "}" >> (Quote o rd o implode) 
11520  1077 
 Scan.repeat1 
1078 
( $$ "'"  Scan.one Symbol.not_eof 

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

1079 
 Scan.unless ($$ "_"  $$ "?"  $$ "\\<module>"  $$ "/"  $$ "{"  $$ "*") 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

1080 
(Scan.one Symbol.not_eof)) >> (Pretty o str o implode))) 
11520  1081 
(Symbol.explode s) of 
1082 
(p, []) => p 

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

1084 

15801  1085 
val _ = Context.add_setup 
18708  1086 
(assoc_types [("fun", (parse_mixfix (K dummyT) "(_ >/ _)", 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1087 
[("term_of", 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1088 
"fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T > U);\n"), 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1089 
("test", 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1090 
"fun gen_fun_type _ G i =\n\ 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1091 
\ let\n\ 
18679  1092 
\ val f = ref (fn x => raise Match);\n\ 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1093 
\ val _ = (f := (fn x =>\n\ 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

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

1095 
\ val y = G i;\n\ 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1096 
\ val f' = !f\n\ 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1097 
\ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ 
18708  1098 
\ in (fn x => !f x) end;\n")]))]); 
15801  1099 

1100 

17057  1101 
structure P = OuterParse and K = OuterKeyword; 
11520  1102 

17144  1103 
fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ") 
1104 
(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

1105 

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

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

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

1109 

11520  1110 
val assoc_typeP = 
1111 
OuterSyntax.command "types_code" 

11546  1112 
"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

1113 
(Scan.repeat1 (P.xname  P.$$$ "("  P.string  P.$$$ ")"  parse_attach) >> 
12452  1114 
(fn xs => Toplevel.theory (fn thy => assoc_types 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1115 
(map (fn ((name, mfx), aux) => (name, (parse_mixfix 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1116 
(typ_of o read_ctyp thy) mfx, aux))) xs) thy))); 
11520  1117 

1118 
val assoc_constP = 

1119 
OuterSyntax.command "consts_code" 

11546  1120 
"associate constants with target language code" K.thy_decl 
11520  1121 
(Scan.repeat1 
13003  1122 
(P.xname  (Scan.option (P.$$$ "::"  P.typ))  
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1123 
P.$$$ "("  P.string  P.$$$ ")"  parse_attach) >> 
11520  1124 
(fn xs => Toplevel.theory (fn thy => assoc_consts 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1125 
(map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix 
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1126 
(term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) 
11520  1127 
xs) thy))); 
1128 

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

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

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

1133 
(if lib then Scan.succeed [] 

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

1135 
P.$$$ "contains"  

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

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

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

1139 
let 

1140 
val mode'' = if lib then "library" ins (mode' \ "library") 

1141 
else mode' \ "library"; 

1142 
val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs 

1143 
in ((case opt_fname of 

1144 
NONE => use_text Context.ml_output false 

1145 
(space_implode "\n" (map snd code)) 

1146 
 SOME fname => 

1147 
if lib then 

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

1149 
(Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) 

1150 
(("ROOT", implode (map (fn (name, _) => 

1151 
"use \"" ^ name ^ ".ML\";\n") code)) :: code) 

1152 
else File.write (Path.unpack fname) (snd (hd code))); 

1153 
if lib then thy 

17412  1154 
else map_modules (Symtab.update (module, gr)) thy) 
17144  1155 
end)); 
1156 

1157 
val code_libraryP = 

1158 
OuterSyntax.command "code_library" 

1159 
"generates code for terms (one structure for each theory)" K.thy_decl 

1160 
(parse_code true); 

1161 

1162 
val code_moduleP = 

1163 
OuterSyntax.command "code_module" 

1164 
"generates code for terms (single structure, incremental)" K.thy_decl 

1165 
(parse_code false); 

11520  1166 

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

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

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

1171 

1172 
val parse_test_params = P.short_ident : (fn s => 

17521  1173 
P.$$$ "="  (AList.lookup (op =) params s > the_default Scan.fail)) >> snd; 
14105  1174 

1175 
fun parse_tyinst xs = 

16458  1176 
(P.type_ident  P.$$$ "="  P.typ >> (fn (v, s) => fn thy => 
1177 
fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs; 

14105  1178 

1179 
fun app [] x = x 

1180 
 app (f :: fs) x = app fs (f x); 

1181 

1182 
val test_paramsP = 

1183 
OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl 

1184 
(P.$$$ "["  P.list1 parse_test_params  P.$$$ "]" >> 

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

16649  1186 
map_test_params (app (map (fn f => f thy) fs)) thy))); 
14105  1187 

1188 
val testP = 

1189 
OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag 

1190 
(Scan.option (P.$$$ "["  P.list1 

16458  1191 
( parse_test_params >> (fn f => fn thy => apfst (f thy)) 
14105  1192 
 parse_tyinst)  P.$$$ "]")  Scan.optional P.nat 1 >> 
1193 
(fn (ps, g) => Toplevel.keep (fn st => 

15570  1194 
test_goal (app (getOpt (Option.map 
18664  1195 
(map (fn f => f (Toplevel.theory_of st))) ps, [])) 
14105  1196 
(get_test_params (Toplevel.theory_of st), [])) g st))); 
1197 

17549  1198 
val valueP = 
1199 
OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag 

1200 
(P.term >> (Toplevel.no_timing oo print_evaluated_term)); 

1201 

17144  1202 
val _ = OuterSyntax.add_keywords ["attach", "file", "contains"]; 
16769
7f188f2127f7
Implemented mechanism for attaching auxiliary code to consts_code and
berghofe
parents:
16649
diff
changeset

1203 

15801  1204 
val _ = OuterSyntax.add_parsers 
17549  1205 
[assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP]; 
11520  1206 

1207 
end; 