author  wenzelm 
Fri, 21 May 2004 21:15:45 +0200  
changeset 14769  b698d0b243dc 
parent 14598  7009f59711e3 
child 14818  ad83019a66a4 
permissions  rwrr 
11520  1 
(* Title: Pure/codegen.ML 
2 
ID: $Id$ 

11539  3 
Author: Stefan Berghofer, TU Muenchen 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

11520  5 

11539  6 
Generic code generator. 
11520  7 
*) 
8 

9 
signature CODEGEN = 

10 
sig 

11 
val quiet_mode : bool ref 

12 
val message : string > unit 

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

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

14 
val margin : int ref 
11520  15 

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

19 
 Pretty of Pretty.T 

12452  20 
 Quote of 'a; 
11520  21 

12452  22 
type 'a codegen 
23 

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

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

14197  26 
val add_attribute: string > (Args.T list > theory attribute * Args.T list) > theory > theory 
11520  27 
val print_codegens: theory > unit 
28 
val generate_code: theory > (string * string) list > string 

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

12452  30 
val assoc_consts: (xstring * string option * term mixfix list) list > theory > theory 
31 
val assoc_consts_i: (xstring * typ option * term mixfix list) list > theory > theory 

32 
val assoc_types: (xstring * typ mixfix list) list > theory > theory 

33 
val get_assoc_code: theory > string > typ > term mixfix list option 

34 
val get_assoc_type: theory > string > typ mixfix list option 

35 
val invoke_codegen: theory > string > bool > 

36 
(exn option * string) Graph.T * term > (exn option * string) Graph.T * Pretty.T 

37 
val invoke_tycodegen: theory > string > bool > 

38 
(exn option * string) Graph.T * typ > (exn option * string) Graph.T * Pretty.T 

11520  39 
val mk_const_id: Sign.sg > string > string 
40 
val mk_type_id: Sign.sg > string > string 

41 
val rename_term: term > term 

42 
val get_defn: theory > string > typ > ((term list * term) * int option) option 

43 
val is_instance: theory > typ > typ > bool 

44 
val parens: Pretty.T > Pretty.T 

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

46 
val eta_expand: term > term list > int > term 

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

48 
val mk_type: bool > typ > Pretty.T 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

49 
val mk_term_of: Sign.sg > bool > typ > Pretty.T 
14105  50 
val mk_gen: Sign.sg > bool > string list > string > typ > Pretty.T 
51 
val test_fn: (int > (string * term) list option) ref 

52 
val test_term: theory > int > int > term > (string * term) list option 

12452  53 
val parse_mixfix: (string > 'a) > string > 'a mixfix list 
11520  54 
val parsers: OuterSyntax.parser list 
55 
val setup: (theory > theory) list 

56 
end; 

57 

58 
structure Codegen : CODEGEN = 

59 
struct 

60 

61 
val quiet_mode = ref true; 

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

63 

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

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

65 

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

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

67 

11520  68 
(**** Mixfix syntax ****) 
69 

12452  70 
datatype 'a mixfix = 
11520  71 
Arg 
72 
 Ignore 

73 
 Pretty of Pretty.T 

12452  74 
 Quote of 'a; 
11520  75 

76 
fun is_arg Arg = true 

77 
 is_arg Ignore = true 

78 
 is_arg _ = false; 

79 

12452  80 
fun quotes_of [] = [] 
81 
 quotes_of (Quote q :: ms) = q :: quotes_of ms 

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

83 

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

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

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

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

11520  88 

12490  89 
fun num_args x = length (filter is_arg x); 
11520  90 

91 

92 
(**** theory data ****) 

93 

14105  94 
(* type of code generators *) 
11520  95 

12452  96 
type 'a codegen = theory > (exn option * string) Graph.T > 
97 
string > bool > 'a > ((exn option * string) Graph.T * Pretty.T) option; 

98 

14105  99 
(* parameters for random testing *) 
100 

101 
type test_params = 

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

103 

104 
fun merge_test_params 

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

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

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

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

109 
default_type = case default_type1 of 

110 
None => default_type2 

111 
 _ => default_type1}; 

112 

113 
val default_test_params : test_params = 

114 
{size = 10, iterations = 100, default_type = None}; 

115 

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

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

118 

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

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

121 

122 
fun set_default_type s sg ({size, iterations, ...} : test_params) = 

123 
{size = size, iterations = iterations, 

124 
default_type = Some (typ_of (read_ctyp sg s))}; 

125 

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

127 

11520  128 
structure CodegenArgs = 
129 
struct 

130 
val name = "Pure/codegen"; 

131 
type T = 

12452  132 
{codegens : (string * term codegen) list, 
133 
tycodegens : (string * typ codegen) list, 

134 
consts : ((string * typ) * term mixfix list) list, 

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

135 
types : (string * typ mixfix list) list, 
14197  136 
attrs: (string * (Args.T list > theory attribute * Args.T list)) list, 
14105  137 
test_params: test_params}; 
11520  138 

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

139 
val empty = 
14105  140 
{codegens = [], tycodegens = [], consts = [], types = [], attrs = [], 
141 
test_params = default_test_params}; 

11520  142 
val copy = I; 
143 
val prep_ext = I; 

144 

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

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

146 
({codegens = codegens1, tycodegens = tycodegens1, 
14105  147 
consts = consts1, types = types1, attrs = attrs1, 
148 
test_params = test_params1}, 

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

149 
{codegens = codegens2, tycodegens = tycodegens2, 
14105  150 
consts = consts2, types = types2, attrs = attrs2, 
151 
test_params = test_params2}) = 

11520  152 
{codegens = rev (merge_alists (rev codegens1) (rev codegens2)), 
12452  153 
tycodegens = rev (merge_alists (rev tycodegens1) (rev tycodegens2)), 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

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

155 
types = merge_alists types1 types2, 
14105  156 
attrs = merge_alists attrs1 attrs2, 
157 
test_params = merge_test_params test_params1 test_params2}; 

11520  158 

12452  159 
fun print sg ({codegens, tycodegens, ...} : T) = 
160 
Pretty.writeln (Pretty.chunks 

161 
[Pretty.strs ("term code generators:" :: map fst codegens), 

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

11520  163 
end; 
164 

165 
structure CodegenData = TheoryDataFun(CodegenArgs); 

166 
val print_codegens = CodegenData.print; 

167 

168 

14105  169 
(**** access parameters for random testing ****) 
170 

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

172 

173 
fun map_test_params f thy = 

174 
let val {codegens, tycodegens, consts, types, attrs, test_params} = 

175 
CodegenData.get thy; 

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

177 
consts = consts, types = types, attrs = attrs, 

178 
test_params = f test_params} thy 

179 
end; 

180 

181 

12452  182 
(**** add new code generators to theory ****) 
11520  183 

184 
fun add_codegen name f thy = 

14105  185 
let val {codegens, tycodegens, consts, types, attrs, test_params} = 
186 
CodegenData.get thy 

11520  187 
in (case assoc (codegens, name) of 
12452  188 
None => CodegenData.put {codegens = (name, f) :: codegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

189 
tycodegens = tycodegens, consts = consts, types = types, 
14105  190 
attrs = attrs, test_params = test_params} thy 
12452  191 
 Some _ => error ("Code generator " ^ name ^ " already declared")) 
192 
end; 

193 

194 
fun add_tycodegen name f thy = 

14105  195 
let val {codegens, tycodegens, consts, types, attrs, test_params} = 
196 
CodegenData.get thy 

12452  197 
in (case assoc (tycodegens, name) of 
198 
None => CodegenData.put {tycodegens = (name, f) :: tycodegens, 

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

199 
codegens = codegens, consts = consts, types = types, 
14105  200 
attrs = attrs, test_params = test_params} thy 
11520  201 
 Some _ => error ("Code generator " ^ name ^ " already declared")) 
202 
end; 

203 

204 

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

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

206 

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

207 
fun add_attribute name att thy = 
14105  208 
let val {codegens, tycodegens, consts, types, attrs, test_params} = 
209 
CodegenData.get thy 

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

210 
in (case assoc (attrs, name) of 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

211 
None => CodegenData.put {tycodegens = tycodegens, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

212 
codegens = codegens, consts = consts, types = types, 
14105  213 
attrs = (name, att) :: attrs, test_params = test_params} thy 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

214 
 Some _ => error ("Code attribute " ^ name ^ " already declared")) 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

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

216 

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

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

219 
val code_attr = 
14197  220 
Attrib.syntax (Scan.depend (fn thy => foldr op  (map mk_parser 
221 
(#attrs (CodegenData.get thy)), Scan.fail) >> pair thy)); 

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

222 

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

223 

11520  224 
(**** associate constants with target language code ****) 
225 

226 
fun gen_assoc_consts prep_type xs thy = foldl (fn (thy, (s, tyopt, syn)) => 

227 
let 

228 
val sg = sign_of thy; 

14105  229 
val {codegens, tycodegens, consts, types, attrs, test_params} = 
230 
CodegenData.get thy; 

11520  231 
val cname = Sign.intern_const sg s; 
232 
in 

233 
(case Sign.const_type sg cname of 

234 
Some T => 

235 
let val T' = (case tyopt of 

236 
None => T 

237 
 Some ty => 

238 
let val U = prep_type sg ty 

14769  239 
in if Sign.typ_instance sg (U, T) then U 
11520  240 
else error ("Illegal type constraint for constant " ^ cname) 
241 
end) 

242 
in (case assoc (consts, (cname, T')) of 

243 
None => CodegenData.put {codegens = codegens, 

12452  244 
tycodegens = tycodegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

245 
consts = ((cname, T'), syn) :: consts, 
14105  246 
types = types, attrs = attrs, test_params = test_params} thy 
11520  247 
 Some _ => error ("Constant " ^ cname ^ " already associated with code")) 
248 
end 

249 
 _ => error ("Not a constant: " ^ s)) 

250 
end) (thy, xs); 

251 

252 
val assoc_consts_i = gen_assoc_consts (K I); 

253 
val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg); 

254 

255 
(**** associate types with target language types ****) 

256 

257 
fun assoc_types xs thy = foldl (fn (thy, (s, syn)) => 

258 
let 

14105  259 
val {codegens, tycodegens, consts, types, attrs, test_params} = 
260 
CodegenData.get thy; 

11520  261 
val tc = Sign.intern_tycon (sign_of thy) s 
262 
in 

263 
(case assoc (types, tc) of 

12452  264 
None => CodegenData.put {codegens = codegens, 
265 
tycodegens = tycodegens, consts = consts, 

14105  266 
types = (tc, syn) :: types, attrs = attrs, 
267 
test_params = test_params} thy 

11520  268 
 Some _ => error ("Type " ^ tc ^ " already associated with code")) 
269 
end) (thy, xs); 

270 

12452  271 
fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s); 
11546  272 

11520  273 

274 
(**** make valid ML identifiers ****) 

275 

276 
fun gen_mk_id kind rename sg s = 

277 
let 

278 
val (xs as x::_) = explode (rename (space_implode "_" 

279 
(NameSpace.unpack (Sign.cond_extern sg kind s)))); 

280 
fun check_str [] = "" 

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

281 
 check_str (" " :: xs) = "_" ^ check_str xs 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

282 
 check_str (x :: xs) = 
12824  283 
(if Symbol.is_letdig x then x 
11520  284 
else "_" ^ string_of_int (ord x)) ^ check_str xs 
285 
in 

286 
(if not (Symbol.is_letter x) then "id" else "") ^ check_str xs 

287 
end; 

288 

13073
cc9d7f403a4b
mk_const_id now checks for clashes with reserved ML identifiers.
berghofe
parents:
13003
diff
changeset

289 
val mk_const_id = gen_mk_id Sign.constK 
cc9d7f403a4b
mk_const_id now checks for clashes with reserved ML identifiers.
berghofe
parents:
13003
diff
changeset

290 
(fn s => if s mem ThmDatabase.ml_reserved then s ^ "_const" else s); 
cc9d7f403a4b
mk_const_id now checks for clashes with reserved ML identifiers.
berghofe
parents:
13003
diff
changeset

291 

11520  292 
val mk_type_id = gen_mk_id Sign.typeK 
293 
(fn s => if s mem ThmDatabase.ml_reserved then s ^ "_type" else s); 

294 

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

295 
fun rename_terms ts = 
11520  296 
let 
13731
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

297 
val names = foldr add_term_names 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

298 
(ts, map (fst o fst) (Drule.vars_of_terms ts)); 
11520  299 
val clash = names inter ThmDatabase.ml_reserved; 
300 
val ps = clash ~~ variantlist (clash, names); 

301 

302 
fun rename (Var ((a, i), T)) = Var ((if_none (assoc (ps, a)) a, i), T) 

303 
 rename (Free (a, T)) = Free (if_none (assoc (ps, a)) a, T) 

304 
 rename (Abs (s, T, t)) = Abs (s, T, rename t) 

305 
 rename (t $ u) = rename t $ rename u 

306 
 rename t = t; 

307 
in 

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

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

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

310 

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

311 
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

312 

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

313 

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

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

315 

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

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

318 

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

319 
fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) => 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

320 
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

321 

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

322 
fun get_defn thy s T = 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

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

324 
val axms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

325 
(thy :: Theory.ancestors_of thy)); 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

326 
val defs = mapfilter (fn (_, t) => 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

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

328 
val (lhs, rhs) = Logic.dest_equals t; 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

329 
val (c, args) = strip_comb lhs; 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

330 
val (s', T') = dest_Const c 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

331 
in if s=s' then Some (T', split_last (rename_terms (args @ [rhs]))) 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

332 
else None end) handle TERM _ => None) axms; 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

333 
val i = find_index (is_instance thy T o fst) defs 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

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

335 
if i>=0 then Some (snd (nth_elem (i, defs)), 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

336 
if length defs = 1 then None else Some i) 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

337 
else None 
11520  338 
end; 
339 

340 

12452  341 
(**** invoke suitable code generator for term / type ****) 
11520  342 

12452  343 
fun invoke_codegen thy dep brack (gr, t) = (case get_first 
11520  344 
(fn (_, f) => f thy gr dep brack t) (#codegens (CodegenData.get thy)) of 
345 
None => error ("Unable to generate code for term:\n" ^ 

346 
Sign.string_of_term (sign_of thy) t ^ "\nrequired by:\n" ^ 

347 
commas (Graph.all_succs gr [dep])) 

12452  348 
 Some x => x); 
349 

350 
fun invoke_tycodegen thy dep brack (gr, T) = (case get_first 

351 
(fn (_, f) => f thy gr dep brack T) (#tycodegens (CodegenData.get thy)) of 

352 
None => error ("Unable to generate code for type:\n" ^ 

353 
Sign.string_of_typ (sign_of thy) T ^ "\nrequired by:\n" ^ 

354 
commas (Graph.all_succs gr [dep])) 

355 
 Some x => x); 

11520  356 

357 

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

359 

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

361 

362 
fun pretty_fn [] p = [p] 

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

364 
Pretty.brk 1 :: pretty_fn xs p; 

365 

366 
fun pretty_mixfix [] [] _ = [] 

367 
 pretty_mixfix (Arg :: ms) (p :: ps) qs = p :: pretty_mixfix ms ps qs 

12452  368 
 pretty_mixfix (Ignore :: ms) ps qs = pretty_mixfix ms ps qs 
11520  369 
 pretty_mixfix (Pretty p :: ms) ps qs = p :: pretty_mixfix ms ps qs 
12452  370 
 pretty_mixfix (Quote _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs; 
11520  371 

372 

12452  373 
(**** default code generators ****) 
11520  374 

375 
fun eta_expand t ts i = 

376 
let 

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

378 
val j = i  length ts 

379 
in 

380 
foldr (fn (T, t) => Abs ("x", T, t)) 

381 
(take (j, Ts), list_comb (t, ts @ map Bound (j1 downto 0))) 

382 
end; 

383 

384 
fun mk_app _ p [] = p 

385 
 mk_app brack p ps = if brack then 

386 
Pretty.block (Pretty.str "(" :: 

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

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

389 

390 
fun new_names t xs = variantlist (xs, 

391 
map (fst o fst o dest_Var) (term_vars t) union 

392 
add_term_names (t, ThmDatabase.ml_reserved)); 

393 

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

395 

396 
fun default_codegen thy gr dep brack t = 

397 
let 

398 
val (u, ts) = strip_comb t; 

12452  399 
fun codegens brack = foldl_map (invoke_codegen thy dep brack) 
11520  400 
in (case u of 
14105  401 
Var ((s, i), T) => 
402 
let 

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

404 
val (gr'', _) = invoke_tycodegen thy dep false (gr', T) 

405 
in Some (gr'', mk_app brack (Pretty.str (s ^ 

11520  406 
(if i=0 then "" else string_of_int i))) ps) 
407 
end 

408 

14105  409 
 Free (s, T) => 
410 
let 

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

412 
val (gr'', _) = invoke_tycodegen thy dep false (gr', T) 

413 
in Some (gr'', mk_app brack (Pretty.str s) ps) end 

11520  414 

415 
 Const (s, T) => 

416 
(case get_assoc_code thy s T of 

417 
Some ms => 

418 
let val i = num_args ms 

419 
in if length ts < i then 

420 
default_codegen thy gr dep brack (eta_expand u ts i) 

421 
else 

422 
let 

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

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

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

11520  427 
in 
428 
Some (gr3, mk_app brack (Pretty.block (pretty_mixfix ms ps1 ps3)) ps2) 

429 
end 

430 
end 

431 
 None => (case get_defn thy s T of 

432 
None => None 

433 
 Some ((args, rhs), k) => 

434 
let 

435 
val id = mk_const_id (sign_of thy) s ^ (case k of 

436 
None => ""  Some i => "_def" ^ string_of_int i); 

12452  437 
val (gr', ps) = codegens true (gr, ts); 
11520  438 
in 
439 
Some (Graph.add_edge (id, dep) gr' handle Graph.UNDEF _ => 

440 
let 

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

442 
val (Ts, _) = strip_type T; 

443 
val (args', rhs') = 

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

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

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

12452  447 
val (gr1, p) = invoke_codegen thy id false 
448 
(Graph.add_edge (id, dep) 

449 
(Graph.new_node (id, (None, "")) gr'), rhs'); 

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

12580
7fdc00bb2a9e
Code generator now adds type constraints to val declarations (to make
berghofe
parents:
12555
diff
changeset

451 
val (gr3, ty) = invoke_tycodegen thy id false (gr2, T); 
11520  452 
in Graph.map_node id (K (None, Pretty.string_of (Pretty.block 
12580
7fdc00bb2a9e
Code generator now adds type constraints to val declarations (to make
berghofe
parents:
12555
diff
changeset

453 
(separate (Pretty.brk 1) (if null args' then 
7fdc00bb2a9e
Code generator now adds type constraints to val declarations (to make
berghofe
parents:
12555
diff
changeset

454 
[Pretty.str ("val " ^ id ^ " :"), ty] 
7fdc00bb2a9e
Code generator now adds type constraints to val declarations (to make
berghofe
parents:
12555
diff
changeset

455 
else Pretty.str ("fun " ^ id) :: xs) @ 
7fdc00bb2a9e
Code generator now adds type constraints to val declarations (to make
berghofe
parents:
12555
diff
changeset

456 
[Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3 
11520  457 
end, mk_app brack (Pretty.str id) ps) 
458 
end)) 

459 

460 
 Abs _ => 

461 
let 

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

463 
val t = strip_abs_body u 

464 
val bs' = new_names t bs; 

12452  465 
val (gr1, ps) = codegens true (gr, ts); 
466 
val (gr2, p) = invoke_codegen thy dep false 

467 
(gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); 

11520  468 
in 
469 
Some (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ 

470 
[Pretty.str ")"])) ps) 

471 
end 

472 

473 
 _ => None) 

474 
end; 

475 

12452  476 
fun default_tycodegen thy gr dep brack (TVar ((s, i), _)) = 
477 
Some (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i))) 

478 
 default_tycodegen thy gr dep brack (TFree (s, _)) = Some (gr, Pretty.str s) 

479 
 default_tycodegen thy gr dep brack (Type (s, Ts)) = 

480 
(case assoc (#types (CodegenData.get thy), s) of 

481 
None => None 

482 
 Some ms => 

483 
let 

484 
val (gr', ps) = foldl_map 

485 
(invoke_tycodegen thy dep false) (gr, fst (args_of ms Ts)); 

486 
val (gr'', qs) = foldl_map 

487 
(invoke_tycodegen thy dep false) (gr', quotes_of ms) 

488 
in Some (gr'', Pretty.block (pretty_mixfix ms ps qs)) end); 

489 

11520  490 

491 
fun output_code gr xs = implode (map (snd o Graph.get_node gr) 

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

493 

14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14197
diff
changeset

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

495 
setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => 
11520  496 
let 
497 
val sg = sign_of thy; 

498 
val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty; 

499 
val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) 

12452  500 
(invoke_codegen thy "<Top>" false (gr, t))) 
501 
(gr, map (apsnd (prep_term sg)) xs) 

11520  502 
in 
503 
"structure Generated =\nstruct\n\n" ^ 

504 
output_code gr' ["<Top>"] ^ 

505 
space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block 

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

507 
"\n\nend;\n\nopen Generated;\n" 

14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14197
diff
changeset

508 
end)); 
11520  509 

510 
val generate_code_i = gen_generate_code (K I); 

511 
val generate_code = gen_generate_code 

512 
(fn sg => term_of o read_cterm sg o rpair TypeInfer.logicT); 

513 

12452  514 

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

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

516 

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

517 
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

518 

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

519 
fun pretty_list xs = Pretty.block (Pretty.str "[" :: 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

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

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

522 

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

523 
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

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

525 
 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

526 
 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

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

528 
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

529 

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

530 
fun mk_term_of sg 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

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

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

533 
 mk_term_of sg 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

534 
(separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id sg s) :: 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

535 
flat (map (fn T => [mk_term_of sg true T, mk_type true T]) Ts)))); 
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

536 

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

537 

14105  538 
(**** Test data generators ****) 
539 

540 
fun mk_gen sg p xs a (TVar ((s, i), _)) = Pretty.str 

541 
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") 

542 
 mk_gen sg p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") 

543 
 mk_gen sg p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block 

544 
(separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id sg s ^ 

545 
(if s mem xs then "'" else "")) :: map (mk_gen sg true xs a) Ts @ 

546 
(if s mem xs then [Pretty.str a] else [])))); 

547 

548 
val test_fn : (int > (string * term) list option) ref = ref (fn _ => None); 

549 

550 
fun test_term thy sz i t = 

551 
let 

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

553 
"Term to be tested contains type variables"; 

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

555 
"Term to be tested contains schematic variables"; 

556 
val sg = sign_of thy; 

557 
val frees = map dest_Free (term_frees t); 

14140
ca089b9d13c4
test_term now renames variable for size of test data to avoid clashes
berghofe
parents:
14135
diff
changeset

558 
val szname = variant (map fst frees) "i"; 
14105  559 
val s = "structure TestTerm =\nstruct\n\n" ^ 
560 
setmp mode ["term_of", "test"] (generate_code_i thy) 

561 
[("testf", list_abs_free (frees, t))] ^ 

562 
"\n" ^ Pretty.string_of 

563 
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=", 

14140
ca089b9d13c4
test_term now renames variable for size of test data to avoid clashes
berghofe
parents:
14135
diff
changeset

564 
Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1, 
14105  565 
Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, 
566 
Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) => 

567 
Pretty.block [Pretty.str ("val " ^ s ^ " ="), Pretty.brk 1, 

568 
mk_gen sg false [] "" T, Pretty.brk 1, 

14140
ca089b9d13c4
test_term now renames variable for size of test data to avoid clashes
berghofe
parents:
14135
diff
changeset

569 
Pretty.str (szname ^ ";")]) frees)), 
14105  570 
Pretty.brk 1, Pretty.str "in", Pretty.brk 1, 
571 
Pretty.block [Pretty.str "if ", 

572 
mk_app false (Pretty.str "testf") (map (Pretty.str o fst) frees), 

14110
c45c94fa16f4
use Library.Some/None instead of just Some/None in generated quickcheck code
kleing
parents:
14105
diff
changeset

573 
Pretty.brk 1, Pretty.str "then Library.None", 
14105  574 
Pretty.brk 1, Pretty.str "else ", 
14110
c45c94fa16f4
use Library.Some/None instead of just Some/None in generated quickcheck code
kleing
parents:
14105
diff
changeset

575 
Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" :: 
14105  576 
flat (separate [Pretty.str ",", Pretty.brk 1] 
577 
(map (fn (s, T) => [Pretty.block 

14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14197
diff
changeset

578 
[Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1, 
14105  579 
mk_app false (mk_term_of sg false T) 
580 
[Pretty.str s], Pretty.str ")"]]) frees)) @ 

581 
[Pretty.str "]"])]], 

582 
Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ 

583 
"\n\nend;\n"; 

584 
val _ = use_text Context.ml_output false s; 

585 
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

586 
else (case (f () handle Match => 
f8a25218b423
test_term now handles Match exception raised in generated code.
berghofe
parents:
14110
diff
changeset

587 
(warning "Exception Match raised in generated code"; None)) of 
f8a25218b423
test_term now handles Match exception raised in generated code.
berghofe
parents:
14110
diff
changeset

588 
None => iter f (k+1)  Some x => Some x); 
14105  589 
fun test k = if k > sz then None 
590 
else (priority ("Test data size: " ^ string_of_int k); 

591 
case iter (fn () => !test_fn k) 1 of 

592 
None => test (k+1)  Some x => Some x); 

593 
in test 0 end; 

594 

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

596 
let 

597 
val sg = Toplevel.sign_of st; 

598 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 

599 
 strip t = t; 

600 
val (gi, frees) = Logic.goal_params 

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

602 
val gi' = ObjectLogic.atomize_term sg (map_term_types 

603 
(map_type_tfree (fn p as (s, _) => if_none (assoc (tvinsts, s)) 

604 
(if_none default_type (TFree p)))) (subst_bounds (frees, strip gi))); 

605 
in case test_term (Toplevel.theory_of st) size iterations gi' of 

606 
None => writeln "No counterexamples found." 

607 
 Some cex => writeln ("Counterexample found:\n" ^ 

608 
Pretty.string_of (Pretty.chunks (map (fn (s, t) => 

609 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, 

610 
Sign.pretty_term sg t]) cex))) 

611 
end; 

612 

613 

12452  614 
(**** Interface ****) 
615 

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

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

617 

11520  618 
fun parse_mixfix rd s = 
619 
(case Scan.finite Symbol.stopper (Scan.repeat 

620 
( $$ "_" >> K Arg 

621 
 $$ "?" >> K Ignore 

622 
 $$ "/"  Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length) 

623 
 $$ "{"  $$ "*"  Scan.repeat1 

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

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

12452  626 
$$ "*"  $$ "}" >> (Quote o rd o implode) 
11520  627 
 Scan.repeat1 
628 
( $$ "'"  Scan.one Symbol.not_eof 

629 
 Scan.unless ($$ "_"  $$ "?"  $$ "/"  $$ "{"  $$ "*") 

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

630 
(Scan.one Symbol.not_eof)) >> (Pretty o str o implode))) 
11520  631 
(Symbol.explode s) of 
632 
(p, []) => p 

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

634 

11546  635 
structure P = OuterParse and K = OuterSyntax.Keyword; 
11520  636 

637 
val assoc_typeP = 

638 
OuterSyntax.command "types_code" 

11546  639 
"associate types with target language types" K.thy_decl 
11520  640 
(Scan.repeat1 (P.xname  P.$$$ "("  P.string  P.$$$ ")") >> 
12452  641 
(fn xs => Toplevel.theory (fn thy => assoc_types 
642 
(map (fn (name, mfx) => (name, parse_mixfix 

643 
(typ_of o read_ctyp (sign_of thy)) mfx)) xs) thy))); 

11520  644 

645 
val assoc_constP = 

646 
OuterSyntax.command "consts_code" 

11546  647 
"associate constants with target language code" K.thy_decl 
11520  648 
(Scan.repeat1 
13003  649 
(P.xname  (Scan.option (P.$$$ "::"  P.typ))  
11520  650 
P.$$$ "("  P.string  P.$$$ ")") >> 
651 
(fn xs => Toplevel.theory (fn thy => assoc_consts 

652 
(map (fn ((name, optype), mfx) => (name, optype, parse_mixfix 

653 
(term_of o read_cterm (sign_of thy) o rpair TypeInfer.logicT) mfx)) 

654 
xs) thy))); 

655 

656 
val generate_codeP = 

11546  657 
OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl 
13003  658 
(Scan.option (P.$$$ "("  P.name  P.$$$ ")")  
13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

659 
Scan.optional (P.$$$ "["  P.enum "," P.xname  P.$$$ "]") (!mode)  
13003  660 
Scan.repeat1 (P.name  P.$$$ "="  P.term) >> 
13753
38b76f457b9c
 Added mode reference variable (may be used to switch on and off specific
berghofe
parents:
13731
diff
changeset

661 
(fn ((opt_fname, mode'), xs) => Toplevel.theory (fn thy => 
11520  662 
((case opt_fname of 
663 
None => use_text Context.ml_output false 

664 
 Some fname => File.write (Path.unpack fname)) 

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

665 
(setmp mode mode' (generate_code thy) xs); thy)))); 
11520  666 

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

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

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

671 

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

673 
P.$$$ "="  if_none (assoc (params, s)) Scan.fail) >> snd; 

674 

675 
fun parse_tyinst xs = 

676 
(P.type_ident  P.$$$ "="  P.typ >> (fn (v, s) => fn sg => 

677 
fn (x, ys) => (x, (v, typ_of (read_ctyp sg s)) :: ys))) xs; 

678 

679 
fun app [] x = x 

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

681 

682 
val test_paramsP = 

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

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

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

686 
map_test_params (app (map (fn f => f (sign_of thy)) fs)) thy))); 

687 

688 
val testP = 

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

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

691 
( parse_test_params >> (fn f => fn sg => apfst (f sg)) 

692 
 parse_tyinst)  P.$$$ "]")  Scan.optional P.nat 1 >> 

693 
(fn (ps, g) => Toplevel.keep (fn st => 

694 
test_goal (app (if_none (apsome 

695 
(map (fn f => f (Toplevel.sign_of st))) ps) []) 

696 
(get_test_params (Toplevel.theory_of st), [])) g st))); 

697 

698 
val parsers = [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP]; 

11520  699 

12452  700 
val setup = 
701 
[CodegenData.init, 

702 
add_codegen "default" default_codegen, 

703 
add_tycodegen "default" default_tycodegen, 

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

704 
assoc_types [("fun", parse_mixfix (K dummyT) "(_ >/ _)")], 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

705 
Attrib.add_attributes [("code", 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

706 
(code_attr, K Attrib.undef_local_attribute), 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

707 
"declare theorems for code generation")]]; 
11520  708 

709 
end; 

710 

711 
OuterSyntax.add_parsers Codegen.parsers; 