author  berghofe 
Sat, 29 Mar 2003 12:28:53 +0100  
changeset 13886  0b243f6e257e 
parent 13753  38b76f457b9c 
child 14105  85d1a908f024 
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 

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

26 
val add_attribute: string > theory attribute > 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 

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

47 
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

48 
val mk_term_of: Sign.sg > bool > typ > Pretty.T 
12452  49 
val parse_mixfix: (string > 'a) > string > 'a mixfix list 
11520  50 
val parsers: OuterSyntax.parser list 
51 
val setup: (theory > theory) list 

52 
end; 

53 

54 
structure Codegen : CODEGEN = 

55 
struct 

56 

57 
val quiet_mode = ref true; 

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

59 

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

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

61 

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

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

63 

11520  64 
(**** Mixfix syntax ****) 
65 

12452  66 
datatype 'a mixfix = 
11520  67 
Arg 
68 
 Ignore 

69 
 Pretty of Pretty.T 

12452  70 
 Quote of 'a; 
11520  71 

72 
fun is_arg Arg = true 

73 
 is_arg Ignore = true 

74 
 is_arg _ = false; 

75 

12452  76 
fun quotes_of [] = [] 
77 
 quotes_of (Quote q :: ms) = q :: quotes_of ms 

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

79 

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

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

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

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

11520  84 

12490  85 
fun num_args x = length (filter is_arg x); 
11520  86 

87 

88 
(**** theory data ****) 

89 

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

91 

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

94 

11520  95 
structure CodegenArgs = 
96 
struct 

97 
val name = "Pure/codegen"; 

98 
type T = 

12452  99 
{codegens : (string * term codegen) list, 
100 
tycodegens : (string * typ codegen) list, 

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

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

102 
types : (string * typ mixfix list) list, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

103 
attrs: (string * theory attribute) list}; 
11520  104 

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

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

106 
{codegens = [], tycodegens = [], consts = [], types = [], attrs = []}; 
11520  107 
val copy = I; 
108 
val prep_ext = I; 

109 

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

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

111 
({codegens = codegens1, tycodegens = tycodegens1, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

112 
consts = consts1, types = types1, attrs = attrs1}, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

113 
{codegens = codegens2, tycodegens = tycodegens2, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

114 
consts = consts2, types = types2, attrs = attrs2}) = 
11520  115 
{codegens = rev (merge_alists (rev codegens1) (rev codegens2)), 
12452  116 
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

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

118 
types = merge_alists types1 types2, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

119 
attrs = merge_alists attrs1 attrs2}; 
11520  120 

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

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

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

11520  125 
end; 
126 

127 
structure CodegenData = TheoryDataFun(CodegenArgs); 

128 
val print_codegens = CodegenData.print; 

129 

130 

12452  131 
(**** add new code generators to theory ****) 
11520  132 

133 
fun add_codegen name f thy = 

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

134 
let val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy 
11520  135 
in (case assoc (codegens, name) of 
12452  136 
None => CodegenData.put {codegens = (name, f) :: codegens, 
12555
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

137 
tycodegens = tycodegens, consts = consts, types = types, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

138 
attrs = attrs} thy 
12452  139 
 Some _ => error ("Code generator " ^ name ^ " already declared")) 
140 
end; 

141 

142 
fun add_tycodegen name f thy = 

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

143 
let val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy 
12452  144 
in (case assoc (tycodegens, name) of 
145 
None => CodegenData.put {tycodegens = (name, f) :: tycodegens, 

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

146 
codegens = codegens, consts = consts, types = types, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

147 
attrs = attrs} thy 
11520  148 
 Some _ => error ("Code generator " ^ name ^ " already declared")) 
149 
end; 

150 

151 

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

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

153 

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

154 
fun add_attribute name att thy = 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

155 
let val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

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

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

158 
codegens = codegens, consts = consts, types = types, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

159 
attrs = (name, att) :: attrs} thy 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

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

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

162 

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

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

164 
Attrib.syntax (Scan.depend (fn thy => Scan.optional Args.name "" >> 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

165 
(fn name => (thy, case assoc (#attrs (CodegenData.get thy), name) of 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

166 
None => error ("Unknown code attribute: " ^ quote name) 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

167 
 Some att => att)))); 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

168 

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

169 

11520  170 
(**** associate constants with target language code ****) 
171 

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

173 
let 

174 
val sg = sign_of thy; 

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

175 
val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy; 
11520  176 
val cname = Sign.intern_const sg s; 
177 
in 

178 
(case Sign.const_type sg cname of 

179 
Some T => 

180 
let val T' = (case tyopt of 

181 
None => T 

182 
 Some ty => 

183 
let val U = prep_type sg ty 

184 
in if Type.typ_instance (Sign.tsig_of sg, U, T) then U 

185 
else error ("Illegal type constraint for constant " ^ cname) 

186 
end) 

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

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

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

190 
consts = ((cname, T'), syn) :: consts, 
e6d7f040fdc7
"code" attribute is now managed by basic code generator module.
berghofe
parents:
12490
diff
changeset

191 
types = types, attrs = attrs} thy 
11520  192 
 Some _ => error ("Constant " ^ cname ^ " already associated with code")) 
193 
end 

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

195 
end) (thy, xs); 

196 

197 
val assoc_consts_i = gen_assoc_consts (K I); 

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

199 

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

201 

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

203 
let 

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

204 
val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy; 
11520  205 
val tc = Sign.intern_tycon (sign_of thy) s 
206 
in 

207 
(case assoc (types, tc) of 

12452  208 
None => CodegenData.put {codegens = codegens, 
209 
tycodegens = tycodegens, consts = consts, 

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

210 
types = (tc, syn) :: types, attrs = attrs} thy 
11520  211 
 Some _ => error ("Type " ^ tc ^ " already associated with code")) 
212 
end) (thy, xs); 

213 

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

11520  216 

217 
(**** make valid ML identifiers ****) 

218 

219 
fun gen_mk_id kind rename sg s = 

220 
let 

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

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

223 
fun check_str [] = "" 

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

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

225 
 check_str (x :: xs) = 
12824  226 
(if Symbol.is_letdig x then x 
11520  227 
else "_" ^ string_of_int (ord x)) ^ check_str xs 
228 
in 

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

230 
end; 

231 

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

232 
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

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

234 

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

237 

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

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

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

241 
(ts, map (fst o fst) (Drule.vars_of_terms ts)); 
11520  242 
val clash = names inter ThmDatabase.ml_reserved; 
243 
val ps = clash ~~ variantlist (clash, names); 

244 

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

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

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

248 
 rename (t $ u) = rename t $ rename u 

249 
 rename t = t; 

250 
in 

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

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

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

253 

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

254 
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

255 

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

256 

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

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

258 

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

259 
fun is_instance thy T1 T2 = 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

260 
Type.typ_instance (Sign.tsig_of (sign_of thy), T1, Type.varifyT T2); 
e2d17090052b
Parameters in definitions are now renamed to avoid clashes with
berghofe
parents:
13073
diff
changeset

261 

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

262 
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

263 
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

264 

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

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

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

267 
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

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

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

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

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

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

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

274 
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

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

276 
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

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

278 
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

279 
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

280 
else None 
11520  281 
end; 
282 

283 

12452  284 
(**** invoke suitable code generator for term / type ****) 
11520  285 

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

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

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

12452  291 
 Some x => x); 
292 

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

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

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

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

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

298 
 Some x => x); 

11520  299 

300 

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

302 

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

304 

305 
fun pretty_fn [] p = [p] 

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

307 
Pretty.brk 1 :: pretty_fn xs p; 

308 

309 
fun pretty_mixfix [] [] _ = [] 

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

12452  311 
 pretty_mixfix (Ignore :: ms) ps qs = pretty_mixfix ms ps qs 
11520  312 
 pretty_mixfix (Pretty p :: ms) ps qs = p :: pretty_mixfix ms ps qs 
12452  313 
 pretty_mixfix (Quote _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs; 
11520  314 

315 

12452  316 
(**** default code generators ****) 
11520  317 

318 
fun eta_expand t ts i = 

319 
let 

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

321 
val j = i  length ts 

322 
in 

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

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

325 
end; 

326 

327 
fun mk_app _ p [] = p 

328 
 mk_app brack p ps = if brack then 

329 
Pretty.block (Pretty.str "(" :: 

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

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

332 

333 
fun new_names t xs = variantlist (xs, 

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

335 
add_term_names (t, ThmDatabase.ml_reserved)); 

336 

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

338 

339 
fun default_codegen thy gr dep brack t = 

340 
let 

341 
val (u, ts) = strip_comb t; 

12452  342 
fun codegens brack = foldl_map (invoke_codegen thy dep brack) 
11520  343 
in (case u of 
344 
Var ((s, i), _) => 

12452  345 
let val (gr', ps) = codegens true (gr, ts) 
11520  346 
in Some (gr', mk_app brack (Pretty.str (s ^ 
347 
(if i=0 then "" else string_of_int i))) ps) 

348 
end 

349 

350 
 Free (s, _) => 

12452  351 
let val (gr', ps) = codegens true (gr, ts) 
11520  352 
in Some (gr', mk_app brack (Pretty.str s) ps) end 
353 

354 
 Const (s, T) => 

355 
(case get_assoc_code thy s T of 

356 
Some ms => 

357 
let val i = num_args ms 

358 
in if length ts < i then 

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

360 
else 

361 
let 

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

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

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

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

368 
end 

369 
end 

370 
 None => (case get_defn thy s T of 

371 
None => None 

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

373 
let 

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

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

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

379 
let 

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

381 
val (Ts, _) = strip_type T; 

382 
val (args', rhs') = 

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

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

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

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

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

389 
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

390 
val (gr3, ty) = invoke_tycodegen thy id false (gr2, T); 
11520  391 
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

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

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

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

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

398 

399 
 Abs _ => 

400 
let 

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

402 
val t = strip_abs_body u 

403 
val bs' = new_names t bs; 

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

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

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

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

410 
end 

411 

412 
 _ => None) 

413 
end; 

414 

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

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

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

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

420 
None => None 

421 
 Some ms => 

422 
let 

423 
val (gr', ps) = foldl_map 

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

425 
val (gr'', qs) = foldl_map 

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

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

428 

11520  429 

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

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

432 

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

433 
fun gen_generate_code prep_term thy = Pretty.setmp_margin (!margin) (fn xs => 
11520  434 
let 
435 
val sg = sign_of thy; 

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

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

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

11520  440 
in 
441 
"structure Generated =\nstruct\n\n" ^ 

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

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

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

445 
"\n\nend;\n\nopen Generated;\n" 

446 
end); 

447 

448 
val generate_code_i = gen_generate_code (K I); 

449 
val generate_code = gen_generate_code 

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

451 

12452  452 

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

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

454 

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

455 
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

456 

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

457 
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

458 
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

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

460 

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

461 
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

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

463 
 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

464 
 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

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

466 
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

467 

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

468 
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

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

470 
 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

471 
 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

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

473 
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

474 

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

475 

12452  476 
(**** Interface ****) 
477 

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

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

479 

11520  480 
fun parse_mixfix rd s = 
481 
(case Scan.finite Symbol.stopper (Scan.repeat 

482 
( $$ "_" >> K Arg 

483 
 $$ "?" >> K Ignore 

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

485 
 $$ "{"  $$ "*"  Scan.repeat1 

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

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

12452  488 
$$ "*"  $$ "}" >> (Quote o rd o implode) 
11520  489 
 Scan.repeat1 
490 
( $$ "'"  Scan.one Symbol.not_eof 

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

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

492 
(Scan.one Symbol.not_eof)) >> (Pretty o str o implode))) 
11520  493 
(Symbol.explode s) of 
494 
(p, []) => p 

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

496 

11546  497 
structure P = OuterParse and K = OuterSyntax.Keyword; 
11520  498 

499 
val assoc_typeP = 

500 
OuterSyntax.command "types_code" 

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

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

11520  506 

507 
val assoc_constP = 

508 
OuterSyntax.command "consts_code" 

11546  509 
"associate constants with target language code" K.thy_decl 
11520  510 
(Scan.repeat1 
13003  511 
(P.xname  (Scan.option (P.$$$ "::"  P.typ))  
11520  512 
P.$$$ "("  P.string  P.$$$ ")") >> 
513 
(fn xs => Toplevel.theory (fn thy => assoc_consts 

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

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

516 
xs) thy))); 

517 

518 
val generate_codeP = 

11546  519 
OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl 
13003  520 
(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

521 
Scan.optional (P.$$$ "["  P.enum "," P.xname  P.$$$ "]") (!mode)  
13003  522 
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

523 
(fn ((opt_fname, mode'), xs) => Toplevel.theory (fn thy => 
11520  524 
((case opt_fname of 
525 
None => use_text Context.ml_output false 

526 
 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

527 
(setmp mode mode' (generate_code thy) xs); thy)))); 
11520  528 

529 
val parsers = [assoc_typeP, assoc_constP, generate_codeP]; 

530 

12452  531 
val setup = 
532 
[CodegenData.init, 

533 
add_codegen "default" default_codegen, 

534 
add_tycodegen "default" default_tycodegen, 

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

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

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

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

538 
"declare theorems for code generation")]]; 
11520  539 

540 
end; 

541 

542 
OuterSyntax.add_parsers Codegen.parsers; 