author  haftmann 
Fri, 04 Dec 2009 18:19:32 +0100  
changeset 33992  bf22ff4f3d19 
parent 33636  a9bb3f063773 
child 34028  1e6206763036 
permissions  rwrr 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

1 
(* Title: Tools/code/code_ml.ML_ 
28054  2 
Author: Florian Haftmann, TU Muenchen 
3 

4 
Serializer for SML and OCaml. 

5 
*) 

6 

7 
signature CODE_ML = 

8 
sig 

32740  9 
val eval: string option > string * (unit > 'a) option Unsynchronized.ref 
30970
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30962
diff
changeset

10 
> ((term > term) > 'a > 'a) > theory > term > string list > 'a 
30947  11 
val target_Eval: string 
28054  12 
val setup: theory > theory 
13 
end; 

14 

15 
structure Code_ML : CODE_ML = 

16 
struct 

17 

18 
open Basic_Code_Thingol; 

19 
open Code_Printer; 

20 

21 
infixr 5 @@; 

22 
infixr 5 @; 

23 

33992  24 

25 
(** generic **) 

26 

28054  27 
val target_SML = "SML"; 
28 
val target_OCaml = "OCaml"; 

30947  29 
val target_Eval = "Eval"; 
28054  30 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

31 
datatype ml_binding = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

32 
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

33 
 ML_Instance of string * ((class * (string * (vname * sort) list)) 
28054  34 
* ((class * (string * (string * dict list list))) list 
28350  35 
* ((string * const) * (thm * bool)) list)); 
28054  36 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

37 
datatype ml_stmt = 
33992  38 
ML_Exc of string * (typscheme * int) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

39 
 ML_Val of ml_binding 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

40 
 ML_Funs of ml_binding list * string list 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

41 
 ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

42 
 ML_Class of string * (vname * ((class * string) list * (string * itype) list)); 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

43 

a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

44 
fun stmt_name_of_binding (ML_Function (name, _)) = name 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

45 
 stmt_name_of_binding (ML_Instance (name, _)) = name; 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

46 

a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

47 
fun stmt_names_of (ML_Exc (name, _)) = [name] 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

48 
 stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding] 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

49 
 stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

50 
 stmt_names_of (ML_Datas ds) = map fst ds 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

51 
 stmt_names_of (ML_Class (name, _)) = [name]; 
28054  52 

33992  53 
fun print_product _ [] = NONE 
54 
 print_product print [x] = SOME (print x) 

55 
 print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs); 

28054  56 

33992  57 
fun print_tuple _ _ [] = NONE 
58 
 print_tuple print fxy [x] = SOME (print fxy x) 

59 
 print_tuple print _ xs = SOME (Pretty.list "(" ")" (map (print NOBR) xs)); 

28054  60 

33992  61 

62 
(** SML serializer **) 

63 

64 
fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = 

28054  65 
let 
33992  66 
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco 
67 
 print_tyco_expr fxy (tyco, [ty]) = 

68 
concat [print_typ BR ty, (str o deresolve) tyco] 

69 
 print_tyco_expr fxy (tyco, tys) = 

70 
concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 

71 
and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco 

72 
of NONE => print_tyco_expr fxy (tyco, tys) 

73 
 SOME (i, print) => print print_typ fxy tys) 

74 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 

75 
fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); 

76 
fun print_typscheme_prefix (vs, p) = Pretty.enum " >" "" "" 

77 
(map_filter (fn (v, sort) => 

78 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

79 
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); 

80 
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); 

81 
fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) = 

82 
brackify fxy ((str o deresolve) inst :: 

83 
(if is_pseudo_fun inst then [str "()"] 

84 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

85 
 print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) = 

86 
let 

87 
val v_p = str (if k = 1 then first_upper v ^ "_" 

88 
else first_upper v ^ string_of_int (i+1) ^ "_"); 

89 
in case classrels 

90 
of [] => v_p 

91 
 [classrel] => brackets [(str o deresolve) classrel, v_p] 

92 
 classrels => brackets 

93 
[Pretty.enum " o" "(" ")" (map (str o deresolve) classrels), v_p] 

94 
end 

95 
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); 

96 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 

97 
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); 

98 
fun print_term is_pseudo_fun thm vars fxy (IConst c) = 

99 
print_app is_pseudo_fun thm vars fxy (c, []) 

100 
 print_term is_pseudo_fun thm vars fxy (IVar NONE) = 

31889  101 
str "_" 
33992  102 
 print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

103 
str (lookup_var vars v) 
33992  104 
 print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = 
28054  105 
(case Code_Thingol.unfold_const_app t 
33992  106 
of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts 
107 
 NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1, 

108 
print_term is_pseudo_fun thm vars BR t2]) 

109 
 print_term is_pseudo_fun thm vars fxy (t as _ `=> _) = 

28054  110 
let 
31874  111 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
33992  112 
fun print_abs (pat, ty) = 
113 
print_bind is_pseudo_fun thm NOBR pat 

28054  114 
#>> (fn p => concat [str "fn", p, str "=>"]); 
33992  115 
val (ps, vars') = fold_map print_abs binds vars; 
116 
in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end 

117 
 print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = 

28054  118 
(case Code_Thingol.unfold_const_app t0 
119 
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) 

33992  120 
then print_case is_pseudo_fun thm vars fxy cases 
121 
else print_app is_pseudo_fun thm vars fxy c_ts 

122 
 NONE => print_case is_pseudo_fun thm vars fxy cases) 

123 
and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = 

29175  124 
if is_cons c then 
33992  125 
let val k = length tys in 
126 
if k < 2 orelse length ts = k 

127 
then (str o deresolve) c 

128 
:: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts) 

129 
else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] 

130 
end 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

131 
else if is_pseudo_fun c 
29175  132 
then (str o deresolve) c @@ str "()" 
33992  133 
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss 
134 
@ map (print_term is_pseudo_fun thm vars BR) ts 

135 
and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

136 
(print_term is_pseudo_fun) syntax_const thm vars 

137 
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) 

138 
and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = 

28054  139 
let 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29264
diff
changeset

140 
val (binds, body) = Code_Thingol.unfold_let (ICase cases); 
33992  141 
fun print_match ((pat, ty), t) vars = 
28054  142 
vars 
33992  143 
> print_bind is_pseudo_fun thm NOBR pat 
144 
>> (fn p => semicolon [str "val", p, str "=", 

145 
print_term is_pseudo_fun thm vars NOBR t]) 

146 
val (ps, vars') = fold_map print_match binds vars; 

28054  147 
in 
148 
Pretty.chunks [ 

33992  149 
Pretty.block [str ("let"), Pretty.fbrk, Pretty.chunks ps], 
150 
Pretty.block [str ("in"), Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], 

28054  151 
str ("end") 
152 
] 

153 
end 

33992  154 
 print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = 
28054  155 
let 
33992  156 
fun print_select delim (pat, body) = 
28054  157 
let 
33992  158 
val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars; 
28054  159 
in 
33992  160 
concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body] 
28054  161 
end; 
162 
in 

31665  163 
brackets ( 
28054  164 
str "case" 
33992  165 
:: print_term is_pseudo_fun thm vars NOBR t 
166 
:: print_select "of" clause 

167 
:: map (print_select "") clauses 

28054  168 
) 
169 
end 

33992  170 
 print_case is_pseudo_fun thm vars fxy ((_, []), _) = 
31121  171 
(concat o map str) ["raise", "Fail", "\"empty case\""]; 
33992  172 
fun print_val_decl print_typscheme (name, typscheme) = concat 
173 
[str "val", str (deresolve name), str ":", print_typscheme typscheme]; 

174 
fun print_datatype_decl definer (tyco, (vs, cos)) = 

175 
let 

176 
fun print_co (co, []) = str (deresolve co) 

177 
 print_co (co, tys) = concat [str (deresolve co), str "of", 

178 
Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 

179 
in 

180 
concat ( 

181 
str definer 

182 
:: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs) 

183 
:: str "=" 

184 
:: separate (str "") (map print_co cos) 

185 
) 

186 
end; 

187 
fun print_def is_pseudo_fun needs_typ definer 

188 
(ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) = 

29189  189 
let 
33992  190 
fun print_eqn definer ((ts, t), (thm, _)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

191 
let 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

192 
val consts = fold Code_Thingol.add_constnames (t :: ts) []; 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

193 
val vars = reserved 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

194 
> intro_base_names 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

195 
(is_none o syntax_const) deresolve consts 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

196 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

197 
(insert (op =)) ts []); 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

198 
val prolog = if needs_typ then 
33992  199 
concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

200 
else Pretty.strs [definer, deresolve name]; 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

201 
in 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

202 
concat ( 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

203 
prolog 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

204 
:: (if is_pseudo_fun name then [str "()"] 
33992  205 
else print_dict_args vs 
206 
@ map (print_term is_pseudo_fun thm vars BR) ts) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

207 
@ str "=" 
33992  208 
@@ print_term is_pseudo_fun thm vars NOBR t 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

209 
) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

210 
end 
33992  211 
val shift = if null eqs then I else 
212 
map (Pretty.block o single o Pretty.block o single); 

213 
in pair 

214 
(print_val_decl print_typscheme (name, vs_ty)) 

215 
((Pretty.block o Pretty.fbreaks o shift) ( 

216 
print_eqn definer eq 

217 
:: map (print_eqn "") eqs 

218 
)) 

29189  219 
end 
33992  220 
 print_def is_pseudo_fun _ definer 
221 
(ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) = 

29189  222 
let 
33992  223 
fun print_superinst (_, (classrel, dss)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

224 
concat [ 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

225 
(str o Long_Name.base_name o deresolve) classrel, 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

226 
str "=", 
33992  227 
print_dict is_pseudo_fun NOBR (DictConst dss) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

228 
]; 
33992  229 
fun print_classparam ((classparam, c_inst), (thm, _)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

230 
concat [ 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

231 
(str o Long_Name.base_name o deresolve) classparam, 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

232 
str "=", 
33992  233 
print_app (K false) thm reserved NOBR (c_inst, []) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

234 
]; 
33992  235 
in pair 
236 
(print_val_decl print_dicttypscheme 

237 
(inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) 

238 
(concat ( 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

239 
str definer 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

240 
:: (str o deresolve) inst 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

241 
:: (if is_pseudo_fun inst then [str "()"] 
33992  242 
else print_dict_args vs) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

243 
@ str "=" 
33992  244 
:: Pretty.list "{" "}" 
245 
(map print_superinst superinsts @ map print_classparam classparams) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

246 
:: str ":" 
33992  247 
@@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) 
248 
)) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

249 
end; 
33992  250 
fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair 
251 
[print_val_decl print_typscheme (name, vs_ty)] 

252 
((semicolon o map str) ( 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

253 
(if n = 0 then "val" else "fun") 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

254 
:: deresolve name 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

255 
:: replicate n "_" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

256 
@ "=" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

257 
:: "raise" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

258 
:: "Fail" 
33992  259 
@@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name 
260 
)) 

261 
 print_stmt (ML_Val binding) = 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

262 
let 
33992  263 
val (sig_p, p) = print_def (K false) true "val" binding 
264 
in pair 

265 
[sig_p] 

266 
(semicolon [p]) 

267 
end 

268 
 print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = 

269 
let 

270 
val print_def' = print_def (member (op =) pseudo_funs) false; 

271 
fun print_pseudo_fun name = concat [ 

29189  272 
str "val", 
273 
(str o deresolve) name, 

274 
str "=", 

275 
(str o deresolve) name, 

276 
str "();" 

277 
]; 

33992  278 
val (sig_ps, (ps, p)) = (apsnd split_last o split_list) 
279 
(print_def' "fun" binding :: map (print_def' "and") bindings); 

280 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

281 
in pair 

282 
sig_ps 

283 
(Pretty.chunks (ps @ semicolon [p] :: pseudo_ps)) 

284 
end 

285 
 print_stmt (ML_Datas [(tyco, (vs, []))]) = 

286 
let 

287 
val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs); 

288 
in 

289 
pair 

290 
[concat [str "type", ty_p]] 

291 
(concat [str "datatype", ty_p, str "=", str "EMPTY__"]) 

292 
end 

293 
 print_stmt (ML_Datas (data :: datas)) = 

28054  294 
let 
33992  295 
val sig_ps = print_datatype_decl "datatype" data 
296 
:: map (print_datatype_decl "and") datas; 

297 
val (ps, p) = split_last sig_ps; 

298 
in pair 

299 
sig_ps 

300 
(Pretty.chunks (ps @ semicolon [p])) 

301 
end 

302 
 print_stmt (ML_Class (class, (v, (superclasses, classparams)))) = 

28054  303 
let 
33992  304 
fun print_field s p = concat [str s, str ":", p]; 
305 
fun print_proj s p = semicolon 

306 
(map str ["val", s, "=", "#" ^ s, ":"] @ p); 

307 
fun print_superclass_decl (superclass, classrel) = 

308 
print_val_decl print_dicttypscheme 

309 
(classrel, ([(v, [class])], (superclass, ITyVar v))); 

310 
fun print_superclass_field (superclass, classrel) = 

311 
print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v)); 

312 
fun print_superclass_proj (superclass, classrel) = 

313 
print_proj (deresolve classrel) 

314 
(print_dicttypscheme ([(v, [class])], (superclass, ITyVar v))); 

315 
fun print_classparam_decl (classparam, ty) = 

316 
print_val_decl print_typscheme 

317 
(classparam, ([(v, [class])], ty)); 

318 
fun print_classparam_field (classparam, ty) = 

319 
print_field (deresolve classparam) (print_typ NOBR ty); 

320 
fun print_classparam_proj (classparam, ty) = 

321 
print_proj (deresolve classparam) 

322 
(print_typscheme ([(v, [class])], ty)); 

323 
in pair 

324 
(concat [str "type", print_dicttyp (class, ITyVar v)] 

325 
:: map print_superclass_decl superclasses 

326 
@ map print_classparam_decl classparams) 

327 
(Pretty.chunks ( 

28054  328 
concat [ 
329 
str ("type '" ^ v), 

330 
(str o deresolve) class, 

331 
str "=", 

33992  332 
Pretty.list "{" "};" ( 
333 
map print_superclass_field superclasses 

334 
@ map print_classparam_field classparams 

28054  335 
) 
336 
] 

33992  337 
:: map print_superclass_proj superclasses 
338 
@ map print_classparam_proj classparams 

339 
)) 

28054  340 
end; 
33992  341 
in print_stmt end; 
28054  342 

33992  343 
fun print_sml_module name some_decls body = Pretty.chunks2 ( 
344 
Pretty.chunks ( 

345 
str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " =")) 

346 
:: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls 

347 
@ (if is_some some_decls then str "end = struct" else str "struct") 

348 
) 

349 
:: body 

350 
@ str ("end; (*struct " ^ name ^ "*)") 

28054  351 
); 
352 

28064  353 
val literals_sml = Literals { 
354 
literal_char = prefix "#" o quote o ML_Syntax.print_char, 

355 
literal_string = quote o translate_string ML_Syntax.print_char, 

356 
literal_numeral = fn unbounded => fn k => 

357 
if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)" 

358 
else string_of_int k, 

33992  359 
literal_list = Pretty.list "[" "]", 
28064  360 
infix_cons = (7, "::") 
361 
}; 

362 

28054  363 

364 
(** OCaml serializer **) 

365 

33992  366 
fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = 
28054  367 
let 
33992  368 
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco 
369 
 print_tyco_expr fxy (tyco, [ty]) = 

370 
concat [print_typ BR ty, (str o deresolve) tyco] 

371 
 print_tyco_expr fxy (tyco, tys) = 

372 
concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 

373 
and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco 

374 
of NONE => print_tyco_expr fxy (tyco, tys) 

375 
 SOME (i, print) => print print_typ fxy tys) 

376 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 

377 
fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); 

378 
fun print_typscheme_prefix (vs, p) = Pretty.enum " >" "" "" 

379 
(map_filter (fn (v, sort) => 

380 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

381 
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); 

382 
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); 

383 
fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) = 

384 
brackify fxy ((str o deresolve) inst :: 

385 
(if is_pseudo_fun inst then [str "()"] 

386 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

387 
 print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) = 

388 
str (if k = 1 then "_" ^ first_upper v 

389 
else "_" ^ first_upper v ^ string_of_int (i+1)) 

390 
> fold_rev (fn classrel => fn p => 

391 
Pretty.block [p, str ".", (str o deresolve) classrel]) classrels 

392 
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); 

393 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 

394 
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); 

395 
fun print_term is_pseudo_fun thm vars fxy (IConst c) = 

396 
print_app is_pseudo_fun thm vars fxy (c, []) 

397 
 print_term is_pseudo_fun thm vars fxy (IVar NONE) = 

31889  398 
str "_" 
33992  399 
 print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

400 
str (lookup_var vars v) 
33992  401 
 print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = 
28054  402 
(case Code_Thingol.unfold_const_app t 
33992  403 
of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts 
404 
 NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1, 

405 
print_term is_pseudo_fun thm vars BR t2]) 

406 
 print_term is_pseudo_fun thm vars fxy (t as _ `=> _) = 

28054  407 
let 
31874  408 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
33992  409 
val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars; 
410 
in brackets (str "fun" :: ps @ str ">" @@ print_term is_pseudo_fun thm vars' NOBR t') end 

411 
 print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = 

412 
(case Code_Thingol.unfold_const_app t0 

28054  413 
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) 
33992  414 
then print_case is_pseudo_fun thm vars fxy cases 
415 
else print_app is_pseudo_fun thm vars fxy c_ts 

416 
 NONE => print_case is_pseudo_fun thm vars fxy cases) 

417 
and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = 

28054  418 
if is_cons c then 
33992  419 
let val k = length tys in 
420 
if length ts = k 

421 
then (str o deresolve) c 

422 
:: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts) 

423 
else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] 

424 
end 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

425 
else if is_pseudo_fun c 
29175  426 
then (str o deresolve) c @@ str "()" 
33992  427 
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss 
428 
@ map (print_term is_pseudo_fun thm vars BR) ts 

429 
and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

430 
(print_term is_pseudo_fun) syntax_const thm vars 

431 
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) 

432 
and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = 

28054  433 
let 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29264
diff
changeset

434 
val (binds, body) = Code_Thingol.unfold_let (ICase cases); 
33992  435 
fun print_let ((pat, ty), t) vars = 
28054  436 
vars 
33992  437 
> print_bind is_pseudo_fun thm NOBR pat 
28054  438 
>> (fn p => concat 
33992  439 
[str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"]) 
440 
val (ps, vars') = fold_map print_let binds vars; 

31665  441 
in 
442 
brackify_block fxy (Pretty.chunks ps) [] 

33992  443 
(print_term is_pseudo_fun thm vars' NOBR body) 
31665  444 
end 
33992  445 
 print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = 
28054  446 
let 
33992  447 
fun print_select delim (pat, body) = 
28054  448 
let 
33992  449 
val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars; 
450 
in concat [str delim, p, str ">", print_term is_pseudo_fun thm vars' NOBR body] end; 

28054  451 
in 
31665  452 
brackets ( 
28054  453 
str "match" 
33992  454 
:: print_term is_pseudo_fun thm vars NOBR t 
455 
:: print_select "with" clause 

456 
:: map (print_select "") clauses 

28054  457 
) 
458 
end 

33992  459 
 print_case is_pseudo_fun thm vars fxy ((_, []), _) = 
31121  460 
(concat o map str) ["failwith", "\"empty case\""]; 
33992  461 
fun print_val_decl print_typscheme (name, typscheme) = concat 
462 
[str "val", str (deresolve name), str ":", print_typscheme typscheme]; 

463 
fun print_datatype_decl definer (tyco, (vs, cos)) = 

464 
let 

465 
fun print_co (co, []) = str (deresolve co) 

466 
 print_co (co, tys) = concat [str (deresolve co), str "of", 

467 
Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 

468 
in 

469 
concat ( 

470 
str definer 

471 
:: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs) 

472 
:: str "=" 

473 
:: separate (str "") (map print_co cos) 

474 
) 

475 
end; 

476 
fun print_def is_pseudo_fun needs_typ definer 

477 
(ML_Function (name, (vs_ty as (vs, ty), eqs))) = 

28054  478 
let 
33992  479 
fun print_eqn ((ts, t), (thm, _)) = 
28054  480 
let 
32913  481 
val consts = fold Code_Thingol.add_constnames (t :: ts) []; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

482 
val vars = reserved 
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

483 
> intro_base_names 
32913  484 
(is_none o syntax_const) deresolve consts 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

485 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  486 
(insert (op =)) ts []); 
487 
in concat [ 

29189  488 
(Pretty.block o Pretty.commas) 
33992  489 
(map (print_term is_pseudo_fun thm vars NOBR) ts), 
28054  490 
str ">", 
33992  491 
print_term is_pseudo_fun thm vars NOBR t 
28054  492 
] end; 
33992  493 
fun print_eqns is_pseudo [((ts, t), (thm, _))] = 
28054  494 
let 
32913  495 
val consts = fold Code_Thingol.add_constnames (t :: ts) []; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

496 
val vars = reserved 
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

497 
> intro_base_names 
32913  498 
(is_none o syntax_const) deresolve consts 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

499 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  500 
(insert (op =)) ts []); 
501 
in 

502 
concat ( 

29189  503 
(if is_pseudo then [str "()"] 
33992  504 
else map (print_term is_pseudo_fun thm vars BR) ts) 
28054  505 
@ str "=" 
33992  506 
@@ print_term is_pseudo_fun thm vars NOBR t 
28054  507 
) 
508 
end 

33992  509 
 print_eqns _ ((eq as (([_], _), _)) :: eqs) = 
28054  510 
Pretty.block ( 
511 
str "=" 

512 
:: Pretty.brk 1 

513 
:: str "function" 

514 
:: Pretty.brk 1 

33992  515 
:: print_eqn eq 
28054  516 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  517 
o single o print_eqn) eqs 
28054  518 
) 
33992  519 
 print_eqns _ (eqs as eq :: eqs') = 
28054  520 
let 
32913  521 
val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) []; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

522 
val vars = reserved 
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

523 
> intro_base_names 
32926  524 
(is_none o syntax_const) deresolve consts; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

525 
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs; 
28054  526 
in 
527 
Pretty.block ( 

528 
Pretty.breaks dummy_parms 

529 
@ Pretty.brk 1 

530 
:: str "=" 

531 
:: Pretty.brk 1 

532 
:: str "match" 

533 
:: Pretty.brk 1 

534 
:: (Pretty.block o Pretty.commas) dummy_parms 

535 
:: Pretty.brk 1 

536 
:: str "with" 

537 
:: Pretty.brk 1 

33992  538 
:: print_eqn eq 
28054  539 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  540 
o single o print_eqn) eqs' 
28054  541 
) 
542 
end; 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

543 
val prolog = if needs_typ then 
33992  544 
concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

545 
else Pretty.strs [definer, deresolve name]; 
33992  546 
in pair 
547 
(print_val_decl print_typscheme (name, vs_ty)) 

548 
(concat ( 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

549 
prolog 
33992  550 
:: print_dict_args vs 
551 
@ print_eqns (is_pseudo_fun name) eqs 

552 
)) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

553 
end 
33992  554 
 print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

555 
let 
33992  556 
fun print_superinst (_, (classrel, dss)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

557 
concat [ 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

558 
(str o deresolve) classrel, 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

559 
str "=", 
33992  560 
print_dict is_pseudo_fun NOBR (DictConst dss) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

561 
]; 
33992  562 
fun print_classparam ((classparam, c_inst), (thm, _)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

563 
concat [ 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

564 
(str o deresolve) classparam, 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

565 
str "=", 
33992  566 
print_app (K false) thm reserved NOBR (c_inst, []) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

567 
]; 
33992  568 
in pair 
569 
(print_val_decl print_dicttypscheme 

570 
(inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) 

571 
(concat ( 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

572 
str definer 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

573 
:: (str o deresolve) inst 
33992  574 
:: print_dict_args vs 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

575 
@ str "=" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

576 
@@ brackets [ 
33992  577 
enum_default "()" ";" "{" "}" (map print_superinst superinsts 
578 
@ map print_classparam classparams), 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

579 
str ":", 
33992  580 
print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

581 
] 
33992  582 
)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

583 
end; 
33992  584 
fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair 
585 
[print_val_decl print_typscheme (name, vs_ty)] 

586 
((doublesemicolon o map str) ( 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

587 
"let" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

588 
:: deresolve name 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

589 
:: replicate n "_" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

590 
@ "=" 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

591 
:: "failwith" 
33992  592 
@@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name 
593 
)) 

594 
 print_stmt (ML_Val binding) = 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

595 
let 
33992  596 
val (sig_p, p) = print_def (K false) true "let" binding 
597 
in pair 

598 
[sig_p] 

599 
(doublesemicolon [p]) 

600 
end 

601 
 print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = 

602 
let 

603 
val print_def' = print_def (member (op =) pseudo_funs) false; 

604 
fun print_pseudo_fun name = concat [ 

29189  605 
str "let", 
606 
(str o deresolve) name, 

607 
str "=", 

608 
(str o deresolve) name, 

609 
str "();;" 

610 
]; 

33992  611 
val (sig_ps, (ps, p)) = (apsnd split_last o split_list) 
612 
(print_def' "let rec" binding :: map (print_def' "and") bindings); 

613 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

614 
in pair 

615 
sig_ps 

616 
(Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps)) 

617 
end 

618 
 print_stmt (ML_Datas [(tyco, (vs, []))]) = 

619 
let 

620 
val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs); 

621 
in 

622 
pair 

623 
[concat [str "type", ty_p]] 

624 
(concat [str "type", ty_p, str "=", str "EMPTY__"]) 

625 
end 

626 
 print_stmt (ML_Datas (data :: datas)) = 

28054  627 
let 
33992  628 
val sig_ps = print_datatype_decl "type" data 
629 
:: map (print_datatype_decl "and") datas; 

630 
val (ps, p) = split_last sig_ps; 

631 
in pair 

632 
sig_ps 

633 
(Pretty.chunks (ps @ doublesemicolon [p])) 

634 
end 

635 
 print_stmt (ML_Class (class, (v, (superclasses, classparams)))) = 

28054  636 
let 
33992  637 
fun print_field s p = concat [str s, str ":", p]; 
638 
fun print_superclass_field (superclass, classrel) = 

639 
print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v)); 

640 
fun print_classparam_decl (classparam, ty) = 

641 
print_val_decl print_typscheme 

642 
(classparam, ([(v, [class])], ty)); 

643 
fun print_classparam_field (classparam, ty) = 

644 
print_field (deresolve classparam) (print_typ NOBR ty); 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

645 
val w = "_" ^ first_upper v; 
33992  646 
fun print_classparam_proj (classparam, _) = 
647 
(concat o map str) ["let", deresolve classparam, w, "=", 

648 
w ^ "." ^ deresolve classparam ^ ";;"]; 

649 
val type_decl_p = concat [ 

650 
str ("type '" ^ v), 

651 
(str o deresolve) class, 

28054  652 
str "=", 
33992  653 
enum_default "unit" ";" "{" "}" ( 
654 
map print_superclass_field superclasses 

655 
@ map print_classparam_field classparams 

656 
) 

28054  657 
]; 
33992  658 
in pair 
659 
(type_decl_p :: map print_classparam_decl classparams) 

660 
(Pretty.chunks ( 

661 
doublesemicolon [type_decl_p] 

662 
:: map print_classparam_proj classparams 

663 
)) 

664 
end; 

665 
in print_stmt end; 

28054  666 

33992  667 
fun print_ocaml_module name some_decls body = Pretty.chunks2 ( 
668 
Pretty.chunks ( 

669 
str ("module " ^ name ^ (if is_some some_decls then " : sig" else " =")) 

670 
:: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls 

671 
@ (if is_some some_decls then str "end = struct" else str "struct") 

672 
) 

673 
:: body 

674 
@ str ("end;; (*struct " ^ name ^ "*)") 

28054  675 
); 
676 

28064  677 
val literals_ocaml = let 
678 
fun chr i = 

679 
let 

680 
val xs = string_of_int i; 

681 
val ys = replicate_string (3  length (explode xs)) "0"; 

682 
in "\\" ^ ys ^ xs end; 

683 
fun char_ocaml c = 

684 
let 

685 
val i = ord c; 

686 
val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126 

687 
then chr i else c 

688 
in s end; 

31377  689 
fun bignum_ocaml k = if k <= 1073741823 
690 
then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" 

691 
else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")" 

28064  692 
in Literals { 
693 
literal_char = enclose "'" "'" o char_ocaml, 

694 
literal_string = quote o translate_string char_ocaml, 

695 
literal_numeral = fn unbounded => fn k => if k >= 0 then 

31377  696 
if unbounded then bignum_ocaml k 
28064  697 
else string_of_int k 
698 
else 

31377  699 
if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")" 
28064  700 
else (enclose "(" ")" o prefix "" o string_of_int o op ~) k, 
701 
literal_list = Pretty.enum ";" "[" "]", 

702 
infix_cons = (6, "::") 

703 
} end; 

704 

705 

28054  706 

707 
(** SML/OCaml generic part **) 

708 

709 
local 

710 

711 
datatype ml_node = 

712 
Dummy of string 

713 
 Stmt of string * ml_stmt 

714 
 Module of string * ((Name.context * Name.context) * ml_node Graph.T); 

715 

716 
in 

717 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

718 
fun ml_node_of_program labelled_name module_name reserved raw_module_alias program = 
28054  719 
let 
720 
val module_alias = if is_some module_name then K module_name else raw_module_alias; 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

721 
val reserved = Name.make_context reserved; 
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

722 
val empty_module = ((reserved, reserved), Graph.empty); 
28054  723 
fun map_node [] f = f 
724 
 map_node (m::ms) f = 

725 
Graph.default_node (m, Module (m, empty_module)) 

726 
#> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) => 

727 
Module (module_name, (nsp, map_node ms f nodes))); 

728 
fun map_nsp_yield [] f (nsp, nodes) = 

729 
let 

730 
val (x, nsp') = f nsp 

731 
in (x, (nsp', nodes)) end 

732 
 map_nsp_yield (m::ms) f (nsp, nodes) = 

733 
let 

734 
val (x, nodes') = 

735 
nodes 

736 
> Graph.default_node (m, Module (m, empty_module)) 

737 
> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 

738 
let 

739 
val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes 

740 
in (x, Module (d_module_name, nsp_nodes')) end) 

741 
in (x, (nsp, nodes')) end; 

742 
fun map_nsp_fun_yield f (nsp_fun, nsp_typ) = 

743 
let 

744 
val (x, nsp_fun') = f nsp_fun 

745 
in (x, (nsp_fun', nsp_typ)) end; 

746 
fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = 

747 
let 

748 
val (x, nsp_typ') = f nsp_typ 

749 
in (x, (nsp_fun, nsp_typ')) end; 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

750 
val mk_name_module = mk_name_module reserved NONE module_alias program; 
28054  751 
fun mk_name_stmt upper name nsp = 
752 
let 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

753 
val (_, base) = dest_name name; 
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

754 
val base' = if upper then first_upper base else base; 
28054  755 
val ([base''], nsp') = Name.variants [base'] nsp; 
756 
in (base'', nsp') end; 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

757 
fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

758 
let 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

759 
val eqs = filter (snd o snd) raw_eqs; 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

760 
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

761 
of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

762 
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

763 
else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

764 
 _ => (eqs, NONE) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

765 
else (eqs, NONE) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

766 
in (ML_Function (name, (tysm, eqs')), is_value) end 
33992  767 
 ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = 
768 
(ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

769 
 ml_binding_of_stmt (name, _) = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

770 
error ("Binding block containing illegal statement: " ^ labelled_name name) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

771 
fun add_fun (name, stmt) = 
29189  772 
let 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

773 
val (binding, some_value_name) = ml_binding_of_stmt (name, stmt); 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

774 
val ml_stmt = case binding 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

775 
of ML_Function (name, ((vs, ty), [])) => 
33992  776 
ML_Exc (name, ((vs, ty), 
777 
(length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

778 
 _ => case some_value_name 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

779 
of NONE => ML_Funs ([binding], []) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

780 
 SOME (name, true) => ML_Funs ([binding], [name]) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

781 
 SOME (name, false) => ML_Val binding 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

782 
in 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

783 
map_nsp_fun_yield (mk_name_stmt false name) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

784 
#>> (fn name' => ([name'], ml_stmt)) 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

785 
end; 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

786 
fun add_funs stmts = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

787 
let 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

788 
val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts > (apsnd o map_filter o Option.map) fst); 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

789 
in 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

790 
fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

791 
#>> rpair ml_stmt 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

792 
end; 
28054  793 
fun add_datatypes stmts = 
794 
fold_map 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

795 
(fn (name, Code_Thingol.Datatype (_, stmt)) => 
28054  796 
map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) 
797 
 (name, Code_Thingol.Datatypecons _) => 

798 
map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE 

799 
 (name, _) => 

800 
error ("Datatype block containing illegal statement: " ^ labelled_name name) 

801 
) stmts 

802 
#>> (split_list #> apsnd (map_filter I 

803 
#> (fn [] => error ("Datatype block without data statement: " 

804 
^ (commas o map (labelled_name o fst)) stmts) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

805 
 stmts => ML_Datas stmts))); 
28054  806 
fun add_class stmts = 
807 
fold_map 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

808 
(fn (name, Code_Thingol.Class (_, stmt)) => 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

809 
map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) 
28054  810 
 (name, Code_Thingol.Classrel _) => 
811 
map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE 

812 
 (name, Code_Thingol.Classparam _) => 

813 
map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE 

814 
 (name, _) => 

815 
error ("Class block containing illegal statement: " ^ labelled_name name) 

816 
) stmts 

817 
#>> (split_list #> apsnd (map_filter I 

818 
#> (fn [] => error ("Class block without class statement: " 

819 
^ (commas o map (labelled_name o fst)) stmts) 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

820 
 [stmt] => ML_Class stmt))); 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

821 
fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

822 
add_fun stmt 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

823 
 add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = 
28054  824 
add_funs stmts 
825 
 add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = 

826 
add_datatypes stmts 

827 
 add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) = 

828 
add_datatypes stmts 

829 
 add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) = 

830 
add_class stmts 

831 
 add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) = 

832 
add_class stmts 

833 
 add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) = 

834 
add_class stmts 

33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

835 
 add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

836 
add_fun stmt 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

837 
 add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) = 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

838 
add_funs stmts 
28054  839 
 add_stmts stmts = error ("Illegal mutual dependencies: " ^ 
840 
(commas o map (labelled_name o fst)) stmts); 

841 
fun add_stmts' stmts nsp_nodes = 

842 
let 

843 
val names as (name :: names') = map fst stmts; 

844 
val deps = 

845 
[] 

846 
> fold (fold (insert (op =)) o Graph.imm_succs program) names 

847 
> subtract (op =) names; 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

848 
val (module_names, _) = (split_list o map dest_name) names; 
28054  849 
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names 
850 
handle Empty => 

851 
error ("Different namespace prefixes for mutual dependencies:\n" 

852 
^ commas (map labelled_name names) 

853 
^ "\n" 

854 
^ commas module_names); 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

855 
val module_name_path = Long_Name.explode module_name; 
28054  856 
fun add_dep name name' = 
857 
let 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

858 
val module_name' = (mk_name_module o fst o dest_name) name'; 
28054  859 
in if module_name = module_name' then 
860 
map_node module_name_path (Graph.add_edge (name, name')) 

861 
else let 

28705  862 
val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =) 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

863 
(module_name_path, Long_Name.explode module_name'); 
28054  864 
in 
865 
map_node common 

866 
(fn node => Graph.add_edge_acyclic (diff1, diff2) node 

867 
handle Graph.CYCLES _ => error ("Dependency " 

868 
^ quote name ^ " > " ^ quote name' 

869 
^ " would result in module dependency cycle")) 

870 
end end; 

871 
in 

872 
nsp_nodes 

873 
> map_nsp_yield module_name_path (add_stmts stmts) 

874 
> (fn (base' :: bases', stmt') => 

875 
apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt'))) 

876 
#> fold2 (fn name' => fn base' => 

877 
Graph.new_node (name', (Dummy base'))) names' bases'))) 

878 
> apsnd (fold (fn name => fold (add_dep name) deps) names) 

879 
> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names) 

880 
end; 

881 
val (_, nodes) = empty_module 

882 
> fold add_stmts' (map (AList.make (Graph.get_node program)) 

883 
(rev (Graph.strong_conn program))); 

884 
fun deresolver prefix name = 

885 
let 

32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

886 
val module_name = (fst o dest_name) name; 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

887 
val module_name' = (Long_Name.explode o mk_name_module) module_name; 
28054  888 
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); 
889 
val stmt_name = 

890 
nodes 

891 
> fold (fn name => fn node => case Graph.get_node node name 

892 
of Module (_, (_, node)) => node) module_name' 

893 
> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name 

894 
 Dummy stmt_name => stmt_name); 

895 
in 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

896 
Long_Name.implode (remainder @ [stmt_name]) 
28054  897 
end handle Graph.UNDEF _ => 
898 
error ("Unknown statement name: " ^ labelled_name name); 

899 
in (deresolver, nodes) end; 

900 

33992  901 
fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name 
902 
reserved includes raw_module_alias _ syntax_tyco syntax_const program stmt_names destination = 

28054  903 
let 
904 
val is_cons = Code_Thingol.is_cons program; 

33992  905 
val presentation_stmt_names = Code_Target.stmt_names_of_destination destination; 
906 
val is_presentation = not (null presentation_stmt_names); 

907 
val module_name = if is_presentation then SOME "Code" else raw_module_name; 

28054  908 
val (deresolver, nodes) = ml_node_of_program labelled_name module_name 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

909 
reserved raw_module_alias program; 
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

910 
val reserved = make_vars reserved; 
33992  911 
fun print_node prefix (Dummy _) = 
28054  912 
NONE 
33992  913 
 print_node prefix (Stmt (_, stmt)) = if is_presentation andalso 
914 
(null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt 

30962  915 
then NONE 
33992  916 
else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt) 
917 
 print_node prefix (Module (module_name, (_, nodes))) = 

918 
let 

919 
val (decls, body) = print_nodes (prefix @ [module_name]) nodes; 

920 
val p = if is_presentation then Pretty.chunks2 body 

921 
else print_module module_name (if with_signatures then SOME decls else NONE) body; 

922 
in SOME ([], p) end 

923 
and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes) 

924 
o rev o flat o Graph.strong_conn) nodes 

925 
> split_list 

926 
> (fn (decls, body) => (flat decls, body)) 

30962  927 
val stmt_names' = (map o try) 
928 
(deresolver (if is_some module_name then the_list module_name else [])) stmt_names; 

33992  929 
val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes)); 
28054  930 
in 
931 
Code_Target.mk_serialization target 

932 
(case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty)  NONE => NONE) 

933 
(fn NONE => Code_Target.code_writeln  SOME file => File.write file o Code_Target.code_of_pretty) 

30962  934 
(rpair stmt_names' o Code_Target.code_of_pretty) p destination 
28054  935 
end; 
936 

937 
end; (*local*) 

938 

939 

940 
(** ML (system language) code for evaluation and instrumentalization **) 

941 

33992  942 
val eval_struct_name = "Code" 
943 

944 
fun eval_code_of some_target with_struct thy = 

945 
let 

946 
val target = the_default target_Eval some_target; 

947 
val serialize = if with_struct then fn _ => fn [] => 

948 
serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true 

949 
else fn _ => fn [] => 

950 
serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true; 

951 
in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end; 

28054  952 

953 

954 
(* evaluation *) 

955 

30970
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30962
diff
changeset

956 
fun eval some_target reff postproc thy t args = 
28054  957 
let 
28275
8dab53900e8c
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28064
diff
changeset

958 
val ctxt = ProofContext.init thy; 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

959 
fun evaluator naming program ((_, (_, ty)), t) deps = 
28054  960 
let 
961 
val _ = if Code_Thingol.contains_dictvar t then 

28724  962 
error "Term to be evaluated contains free dictionaries" else (); 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

963 
val value_name = "Value.VALUE.value" 
28054  964 
val program' = program 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

965 
> Graph.new_node (value_name, 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

966 
Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))]))) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

967 
> fold (curry Graph.add_edge value_name) deps; 
33992  968 
val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name]; 
28054  969 
val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' 
970 
^ space_implode " " (map (enclose "(" ")") args) ^ " end"; 

30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30648
diff
changeset

971 
in ML_Context.evaluate ctxt false reff sml_code end; 
32123
8bac9ee4b28d
integrated add_triv_classes into evaluation stack
haftmann
parents:
31934
diff
changeset

972 
in Code_Thingol.eval thy postproc evaluator t end; 
28054  973 

974 

975 
(* instrumentalization by antiquotation *) 

976 

977 
local 

978 

33519  979 
structure CodeAntiqData = Proof_Data 
28054  980 
( 
30962  981 
type T = (string list * string list) * (bool * (string 
982 
* (string * ((string * string) list * (string * string) list)) lazy)); 

983 
fun init _ = (([], []), (true, ("", Lazy.value ("", ([], []))))); 

28054  984 
); 
985 

986 
val is_first_occ = fst o snd o CodeAntiqData.get; 

987 

30962  988 
fun delayed_code thy tycos consts () = 
28054  989 
let 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

990 
val (consts', (naming, program)) = Code_Thingol.consts_program thy consts; 
30962  991 
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; 
33992  992 
val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos'); 
30962  993 
val (consts'', tycos'') = chop (length consts') target_names; 
994 
val consts_map = map2 (fn const => fn NONE => 

31156  995 
error ("Constant " ^ (quote o Code.string_of_const thy) const 
30962  996 
^ "\nhas a userdefined serialization") 
997 
 SOME const'' => (const, const'')) consts consts'' 

998 
val tycos_map = map2 (fn tyco => fn NONE => 

999 
error ("Type " ^ (quote o Sign.extern_type thy) tyco 

1000 
^ "\nhas a userdefined serialization") 

1001 
 SOME tyco'' => (tyco, tyco'')) tycos tycos''; 

1002 
in (ml_code, (tycos_map, consts_map)) end; 

28054  1003 

30962  1004 
fun register_code new_tycos new_consts ctxt = 
28054  1005 
let 
30962  1006 
val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt; 
1007 
val tycos' = fold (insert (op =)) new_tycos tycos; 

1008 
val consts' = fold (insert (op =)) new_consts consts; 

28054  1009 
val (struct_name', ctxt') = if struct_name = "" 
33992  1010 
then ML_Antiquote.variant eval_struct_name ctxt 
28054  1011 
else (struct_name, ctxt); 
30962  1012 
val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts'); 
1013 
in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end; 

1014 

1015 
fun register_const const = register_code [] [const]; 

28054  1016 

30962  1017 
fun register_datatype tyco constrs = register_code [tyco] constrs; 
1018 

1019 
fun print_const const all_struct_name tycos_map consts_map = 

1020 
(Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const; 

1021 

1022 
fun print_datatype tyco constrs all_struct_name tycos_map consts_map = 

28054  1023 
let 
30962  1024 
val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode; 
1025 
fun check_base name name'' = 

1026 
if upperize (Long_Name.base_name name) = upperize name'' 

1027 
then () else error ("Name as printed " ^ quote name'' 

1028 
^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry."); 

1029 
val tyco'' = (the o AList.lookup (op =) tycos_map) tyco; 

1030 
val constrs'' = map (the o AList.lookup (op =) consts_map) constrs; 

1031 
val _ = check_base tyco tyco''; 

1032 
val _ = map2 check_base constrs constrs''; 

1033 
in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end; 

1034 

1035 
fun print_code struct_name is_first print_it ctxt = 

1036 
let 

1037 
val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt; 

33992  1038 
val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code; 
1039 
val ml_code = if is_first then ml_code 

28054  1040 
else ""; 
30962  1041 
val all_struct_name = Long_Name.append struct_name struct_code_name; 
1042 
in (ml_code, print_it all_struct_name tycos_map consts_map) end; 

28054  1043 

1044 
in 

1045 

1046 
fun ml_code_antiq raw_const {struct_name, background} = 

1047 
let 

31156  1048 
val const = Code.check_const (ProofContext.theory_of background) raw_const; 
28054  1049 
val is_first = is_first_occ background; 
1050 
val background' = register_const const background; 

30962  1051 
in (print_code struct_name is_first (print_const const), background') end; 
1052 

1053 
fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} = 

1054 
let 

1055 
val thy = ProofContext.theory_of background; 

1056 
val tyco = Sign.intern_type thy raw_tyco; 

31156  1057 
val constrs = map (Code.check_const thy) raw_constrs; 
30962  1058 
val constrs' = (map fst o snd o Code.get_datatype thy) tyco; 
33038  1059 
val _ = if eq_set (op =) (constrs, constrs') then () 
30962  1060 
else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors") 
1061 
val is_first = is_first_occ background; 

1062 
val background' = register_datatype tyco constrs background; 

1063 
in (print_code struct_name is_first (print_datatype tyco constrs), background') end; 

28054  1064 

1065 
end; (*local*) 

1066 

1067 

1068 
(** Isar setup **) 

1069 

1070 
val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq); 

30962  1071 
val _ = ML_Context.add_antiq "code_datatype" (fn _ => 
1072 
(Args.tyname  Scan.lift (Args.$$$ "=") 

1073 
 (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "")  Args.term))) 

1074 
>> ml_code_datatype_antiq); 

28054  1075 

1076 
fun isar_seri_sml module_name = 

33992  1077 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
1078 
>> (fn with_signatures => serialize_ml target_SML 

31327  1079 
(SOME (use_text ML_Env.local_context (1, "generated code") false)) 
33992  1080 
print_sml_module print_sml_stmt module_name with_signatures)); 
28054  1081 

1082 
fun isar_seri_ocaml module_name = 

33992  1083 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
1084 
>> (fn with_signatures => serialize_ml target_OCaml NONE 

1085 
print_ocaml_module print_ocaml_stmt module_name with_signatures)); 

28054  1086 

1087 
val setup = 

28064  1088 
Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml)) 
1089 
#> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml)) 

30947  1090 
#> Code_Target.extend_target (target_Eval, (target_SML, K I)) 
33992  1091 
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 
28054  1092 
brackify_infix (1, R) fxy [ 
33992  1093 
print_typ (INFX (1, X)) ty1, 
28054  1094 
str ">", 
33992  1095 
print_typ (INFX (1, R)) ty2 
28054  1096 
])) 
33992  1097 
#> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 
28054  1098 
brackify_infix (1, R) fxy [ 
33992  1099 
print_typ (INFX (1, X)) ty1, 
28054  1100 
str ">", 
33992  1101 
print_typ (INFX (1, R)) ty2 
28054  1102 
])) 
1103 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 

1104 
#> fold (Code_Target.add_reserved target_SML) 

1105 
["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)] 

1106 
#> fold (Code_Target.add_reserved target_OCaml) [ 

1107 
"and", "as", "assert", "begin", "class", 

1108 
"constraint", "do", "done", "downto", "else", "end", "exception", 

1109 
"external", "false", "for", "fun", "function", "functor", "if", 

1110 
"in", "include", "inherit", "initializer", "lazy", "let", "match", "method", 

1111 
"module", "mutable", "new", "object", "of", "open", "or", "private", "rec", 

1112 
"sig", "struct", "then", "to", "true", "try", "type", "val", 

1113 
"virtual", "when", "while", "with" 

1114 
] 

1115 
#> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"]; 

1116 

1117 
end; (*struct*) 