author  haftmann 
Tue, 01 Jun 2010 13:52:11 +0200  
changeset 37242  97097e589715 
parent 36536  8daaa303f90d 
child 37384  5aba26803073 
permissions  rwrr 
36536  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 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

9 
val target_SML: string 
34032  10 
val evaluation_code_of: theory > string > string 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

11 
> Code_Thingol.naming > Code_Thingol.program > string list > string * string option list 
36515  12 
val print_tuple: (Code_Printer.fixity > 'a > Pretty.T) 
13 
> Code_Printer.fixity > 'a list > Pretty.T option 

28054  14 
val setup: theory > theory 
15 
end; 

16 

17 
structure Code_ML : CODE_ML = 

18 
struct 

19 

20 
open Basic_Code_Thingol; 

21 
open Code_Printer; 

22 

23 
infixr 5 @@; 

24 
infixr 5 @; 

25 

33992  26 

27 
(** generic **) 

28 

28054  29 
val target_SML = "SML"; 
30 
val target_OCaml = "OCaml"; 

31 

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

32 
datatype ml_binding = 
35228  33 
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

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

42 
 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

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

44 

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

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

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

47 

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

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

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

50 
 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

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

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

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

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

56 
 print_product print xs = (SOME o enum " *" "" "") (map print xs); 
28054  57 

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

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

60 
 print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); 
28054  61 

33992  62 

63 
(** SML serializer **) 

64 

65 
fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = 

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

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

70 
 print_tyco_expr fxy (tyco, tys) = 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

71 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 
33992  72 
and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco 
73 
of NONE => print_tyco_expr fxy (tyco, tys) 

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

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

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

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

77 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  78 
(map_filter (fn (v, sort) => 
79 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

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

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

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

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

85 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

87 
let 

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

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

90 
in case classrels 

91 
of [] => v_p 

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

93 
 classrels => brackets 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

94 
[enum " o" "(" ")" (map (str o deresolve) classrels), v_p] 
33992  95 
end 
96 
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); 

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

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

35228  99 
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) = 
100 
print_app is_pseudo_fun some_thm vars fxy (c, []) 

101 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  102 
str "_" 
35228  103 
 print_term is_pseudo_fun some_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

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

109 
print_term is_pseudo_fun some_thm vars BR t2]) 

110 
 print_term is_pseudo_fun some_thm vars fxy (t as _ `=> _) = 

28054  111 
let 
31874  112 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
33992  113 
fun print_abs (pat, ty) = 
35228  114 
print_bind is_pseudo_fun some_thm NOBR pat 
28054  115 
#>> (fn p => concat [str "fn", p, str "=>"]); 
33992  116 
val (ps, vars') = fold_map print_abs binds vars; 
35228  117 
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end 
118 
 print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) = 

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

35228  121 
then print_case is_pseudo_fun some_thm vars fxy cases 
122 
else print_app is_pseudo_fun some_thm vars fxy c_ts 

123 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

124 
and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) = 

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

128 
then (str o deresolve) c 

35228  129 
:: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts) 
130 
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] 

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

132 
else if is_pseudo_fun c 
29175  133 
then (str o deresolve) c @@ str "()" 
33992  134 
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss 
35228  135 
@ map (print_term is_pseudo_fun some_thm vars BR) ts 
136 
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

137 
(print_term is_pseudo_fun) syntax_const some_thm vars 

33992  138 
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) 
35228  139 
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) = 
28054  140 
let 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29264
diff
changeset

141 
val (binds, body) = Code_Thingol.unfold_let (ICase cases); 
33992  142 
fun print_match ((pat, ty), t) vars = 
28054  143 
vars 
35228  144 
> print_bind is_pseudo_fun some_thm NOBR pat 
33992  145 
>> (fn p => semicolon [str "val", p, str "=", 
35228  146 
print_term is_pseudo_fun some_thm vars NOBR t]) 
33992  147 
val (ps, vars') = fold_map print_match binds vars; 
28054  148 
in 
149 
Pretty.chunks [ 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

150 
Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], 
35228  151 
Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body], 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

152 
str "end" 
28054  153 
] 
154 
end 

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

31665  164 
brackets ( 
28054  165 
str "case" 
35228  166 
:: print_term is_pseudo_fun some_thm vars NOBR t 
33992  167 
:: print_select "of" clause 
168 
:: map (print_select "") clauses 

28054  169 
) 
170 
end 

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

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

176 
let 

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

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

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

179 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  180 
in 
181 
concat ( 

182 
str definer 

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

184 
:: str "=" 

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

186 
) 

187 
end; 

188 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

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

199 
val prolog = if needs_typ then 
33992  200 
concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

201 
else (concat o map str) [definer, deresolve name]; 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

205 
:: (if is_pseudo_fun name then [str "()"] 
33992  206 
else print_dict_args vs 
35228  207 
@ map (print_term is_pseudo_fun some_thm vars BR) ts) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

214 
in pair 

215 
(print_val_decl print_typscheme (name, vs_ty)) 

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

217 
print_eqn definer eq 

218 
:: map (print_eqn "") eqs 

219 
)) 

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

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

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

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

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

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

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

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

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

235 
]; 
33992  236 
in pair 
237 
(print_val_decl print_dicttypscheme 

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

239 
(concat ( 

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

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

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

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

244 
@ str "=" 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

245 
:: enum "," "{" "}" 
33992  246 
(map print_superinst superinsts @ map print_classparam classparams) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

253 
((semicolon o map str) ( 

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

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

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

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

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

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

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

262 
 print_stmt (ML_Val binding) = 

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

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

266 
[sig_p] 

267 
(semicolon [p]) 

268 
end 

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

270 
let 

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

272 
fun print_pseudo_fun name = concat [ 

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

275 
str "=", 

276 
(str o deresolve) name, 

277 
str "();" 

278 
]; 

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

281 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

282 
in pair 

283 
sig_ps 

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

285 
end 

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

287 
let 

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

289 
in 

290 
pair 

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

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

293 
end 

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

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

298 
val (ps, p) = split_last sig_ps; 

299 
in pair 

300 
sig_ps 

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

302 
end 

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

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

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

308 
fun print_superclass_decl (superclass, classrel) = 

309 
print_val_decl print_dicttypscheme 

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

311 
fun print_superclass_field (superclass, classrel) = 

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

313 
fun print_superclass_proj (superclass, classrel) = 

314 
print_proj (deresolve classrel) 

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

316 
fun print_classparam_decl (classparam, ty) = 

317 
print_val_decl print_typscheme 

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

319 
fun print_classparam_field (classparam, ty) = 

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

321 
fun print_classparam_proj (classparam, ty) = 

322 
print_proj (deresolve classparam) 

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

324 
in pair 

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

326 
:: map print_superclass_decl superclasses 

327 
@ map print_classparam_decl classparams) 

328 
(Pretty.chunks ( 

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

331 
(str o deresolve) class, 

332 
str "=", 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

333 
enum "," "{" "};" ( 
33992  334 
map print_superclass_field superclasses 
335 
@ map print_classparam_field classparams 

28054  336 
) 
337 
] 

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

340 
)) 

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

34032  344 
fun print_sml_module name some_decls body = if name = "" 
345 
then Pretty.chunks2 body 

346 
else Pretty.chunks2 ( 

33992  347 
Pretty.chunks ( 
348 
str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " =")) 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

349 
:: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls 
33992  350 
@ (if is_some some_decls then str "end = struct" else str "struct") 
351 
) 

352 
:: body 

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

28054  354 
); 
355 

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

358 
literal_string = quote o translate_string ML_Syntax.print_char, 

34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

359 
literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)", 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

360 
literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)", 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

361 
literal_naive_numeral = string_of_int, 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

362 
literal_list = enum "," "[" "]", 
28064  363 
infix_cons = (7, "::") 
364 
}; 

365 

28054  366 

367 
(** OCaml serializer **) 

368 

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

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

374 
 print_tyco_expr fxy (tyco, tys) = 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

375 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 
33992  376 
and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco 
377 
of NONE => print_tyco_expr fxy (tyco, tys) 

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

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

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

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

381 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  382 
(map_filter (fn (v, sort) => 
383 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

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

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

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

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

389 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

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

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

393 
> fold_rev (fn classrel => fn p => 

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

395 
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); 

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

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

35228  398 
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) = 
399 
print_app is_pseudo_fun some_thm vars fxy (c, []) 

400 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  401 
str "_" 
35228  402 
 print_term is_pseudo_fun some_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

403 
str (lookup_var vars v) 
35228  404 
 print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = 
28054  405 
(case Code_Thingol.unfold_const_app t 
35228  406 
of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts 
407 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 

408 
print_term is_pseudo_fun some_thm vars BR t2]) 

409 
 print_term is_pseudo_fun some_thm vars fxy (t as _ `=> _) = 

28054  410 
let 
31874  411 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
35228  412 
val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars; 
413 
in brackets (str "fun" :: ps @ str ">" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end 

414 
 print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) = 

33992  415 
(case Code_Thingol.unfold_const_app t0 
28054  416 
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) 
35228  417 
then print_case is_pseudo_fun some_thm vars fxy cases 
418 
else print_app is_pseudo_fun some_thm vars fxy c_ts 

419 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

420 
and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) = 

28054  421 
if is_cons c then 
33992  422 
let val k = length tys in 
423 
if length ts = k 

424 
then (str o deresolve) c 

35228  425 
:: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts) 
426 
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] 

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

428 
else if is_pseudo_fun c 
29175  429 
then (str o deresolve) c @@ str "()" 
33992  430 
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss 
35228  431 
@ map (print_term is_pseudo_fun some_thm vars BR) ts 
432 
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

433 
(print_term is_pseudo_fun) syntax_const some_thm vars 

33992  434 
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) 
35228  435 
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) = 
28054  436 
let 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29264
diff
changeset

437 
val (binds, body) = Code_Thingol.unfold_let (ICase cases); 
33992  438 
fun print_let ((pat, ty), t) vars = 
28054  439 
vars 
35228  440 
> print_bind is_pseudo_fun some_thm NOBR pat 
28054  441 
>> (fn p => concat 
35228  442 
[str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) 
33992  443 
val (ps, vars') = fold_map print_let binds vars; 
31665  444 
in 
445 
brackify_block fxy (Pretty.chunks ps) [] 

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

28054  454 
in 
31665  455 
brackets ( 
28054  456 
str "match" 
35228  457 
:: print_term is_pseudo_fun some_thm vars NOBR t 
33992  458 
:: print_select "with" clause 
459 
:: map (print_select "") clauses 

28054  460 
) 
461 
end 

35228  462 
 print_case is_pseudo_fun some_thm vars fxy ((_, []), _) = 
31121  463 
(concat o map str) ["failwith", "\"empty case\""]; 
33992  464 
fun print_val_decl print_typscheme (name, typscheme) = concat 
465 
[str "val", str (deresolve name), str ":", print_typscheme typscheme]; 

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

467 
let 

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

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

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

470 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  471 
in 
472 
concat ( 

473 
str definer 

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

475 
:: str "=" 

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

477 
) 

478 
end; 

479 
fun print_def is_pseudo_fun needs_typ definer 

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

28054  481 
let 
35228  482 
fun print_eqn ((ts, t), (some_thm, _)) = 
28054  483 
let 
32913  484 
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

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

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

29189  489 
(Pretty.block o Pretty.commas) 
35228  490 
(map (print_term is_pseudo_fun some_thm vars NOBR) ts), 
28054  491 
str ">", 
35228  492 
print_term is_pseudo_fun some_thm vars NOBR t 
28054  493 
] end; 
35228  494 
fun print_eqns is_pseudo [((ts, t), (some_thm, _))] = 
28054  495 
let 
32913  496 
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

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

498 
> intro_base_names 
32913  499 
(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

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

503 
concat ( 

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

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

513 
:: Pretty.brk 1 

514 
:: str "function" 

515 
:: Pretty.brk 1 

33992  516 
:: print_eqn eq 
28054  517 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  518 
o single o print_eqn) eqs 
28054  519 
) 
33992  520 
 print_eqns _ (eqs as eq :: eqs') = 
28054  521 
let 
32913  522 
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

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

524 
> intro_base_names 
32926  525 
(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

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

529 
Pretty.breaks dummy_parms 

530 
@ Pretty.brk 1 

531 
:: str "=" 

532 
:: Pretty.brk 1 

533 
:: str "match" 

534 
:: Pretty.brk 1 

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

536 
:: Pretty.brk 1 

537 
:: str "with" 

538 
:: Pretty.brk 1 

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

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

544 
val prolog = if needs_typ then 
33992  545 
concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

546 
else (concat o map str) [definer, deresolve name]; 
33992  547 
in pair 
548 
(print_val_decl print_typscheme (name, vs_ty)) 

549 
(concat ( 

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

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

553 
)) 

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

554 
end 
33992  555 
 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

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

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

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

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

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

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

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

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

568 
]; 
33992  569 
in pair 
570 
(print_val_decl print_dicttypscheme 

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

572 
(concat ( 

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

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

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

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

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

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

580 
str ":", 
33992  581 
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

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

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

587 
((doublesemicolon o map str) ( 

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

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

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

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

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

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

595 
 print_stmt (ML_Val binding) = 

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

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

599 
[sig_p] 

600 
(doublesemicolon [p]) 

601 
end 

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

603 
let 

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

605 
fun print_pseudo_fun name = concat [ 

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

608 
str "=", 

609 
(str o deresolve) name, 

610 
str "();;" 

611 
]; 

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

614 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

615 
in pair 

616 
sig_ps 

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

618 
end 

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

620 
let 

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

622 
in 

623 
pair 

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

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

626 
end 

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

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

631 
val (ps, p) = split_last sig_ps; 

632 
in pair 

633 
sig_ps 

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

635 
end 

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

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

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

641 
fun print_classparam_decl (classparam, ty) = 

642 
print_val_decl print_typscheme 

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

644 
fun print_classparam_field (classparam, ty) = 

645 
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

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

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

650 
val type_decl_p = concat [ 

651 
str ("type '" ^ v), 

652 
(str o deresolve) class, 

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

656 
@ map print_classparam_field classparams 

657 
) 

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

661 
(Pretty.chunks ( 

662 
doublesemicolon [type_decl_p] 

663 
:: map print_classparam_proj classparams 

664 
)) 

665 
end; 

666 
in print_stmt end; 

28054  667 

34032  668 
fun print_ocaml_module name some_decls body = if name = "" 
669 
then Pretty.chunks2 body 

670 
else Pretty.chunks2 ( 

33992  671 
Pretty.chunks ( 
672 
str ("module " ^ name ^ (if is_some some_decls then " : sig" else " =")) 

34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

673 
:: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls 
33992  674 
@ (if is_some some_decls then str "end = struct" else str "struct") 
675 
) 

676 
:: body 

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

28054  678 
); 
679 

28064  680 
val literals_ocaml = let 
681 
fun chr i = 

682 
let 

683 
val xs = string_of_int i; 

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

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

686 
fun char_ocaml c = 

687 
let 

688 
val i = ord c; 

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

690 
then chr i else c 

691 
in s end; 

34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

692 
fun numeral_ocaml k = if k < 0 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

693 
then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")" 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

694 
else if k <= 1073741823 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

695 
then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

696 
else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")" 
28064  697 
in Literals { 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

698 
literal_char = Library.enclose "'" "'" o char_ocaml, 
28064  699 
literal_string = quote o translate_string char_ocaml, 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

700 
literal_numeral = numeral_ocaml, 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

701 
literal_positive_numeral = numeral_ocaml, 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

702 
literal_naive_numeral = numeral_ocaml, 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

703 
literal_list = enum ";" "[" "]", 
28064  704 
infix_cons = (6, "::") 
705 
} end; 

706 

707 

28054  708 

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

710 

711 
local 

712 

713 
datatype ml_node = 

714 
Dummy of string 

715 
 Stmt of string * ml_stmt 

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

717 

718 
in 

719 

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

720 
fun ml_node_of_program labelled_name module_name reserved raw_module_alias program = 
28054  721 
let 
722 
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

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

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

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

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

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

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

731 
let 

732 
val (x, nsp') = f nsp 

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

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

735 
let 

736 
val (x, nodes') = 

737 
nodes 

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

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

740 
let 

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

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

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

744 
fun map_nsp_fun_yield f (nsp_fun, nsp_typ) = 

745 
let 

746 
val (x, nsp_fun') = f nsp_fun 

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

748 
fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = 

749 
let 

750 
val (x, nsp_typ') = f nsp_typ 

751 
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

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

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

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

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

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

759 
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

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

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

762 
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs 
35228  763 
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty 
764 
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) 

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

765 
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

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

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

768 
in (ML_Function (name, (tysm, eqs')), is_value) end 
33992  769 
 ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = 
770 
(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

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

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

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

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

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

777 
of ML_Function (name, ((vs, ty), [])) => 
33992  778 
ML_Exc (name, ((vs, ty), 
779 
(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

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

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

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

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

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

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

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

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

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

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

790 
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

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

792 
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

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

794 
end; 
28054  795 
fun add_datatypes stmts = 
796 
fold_map 

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

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

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

801 
 (name, _) => 

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

803 
) stmts 

804 
#>> (split_list #> apsnd (map_filter I 

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

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

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

807 
 stmts => ML_Datas stmts))); 
28054  808 
fun add_class stmts = 
809 
fold_map 

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

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

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

814 
 (name, Code_Thingol.Classparam _) => 

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

816 
 (name, _) => 

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

818 
) stmts 

819 
#>> (split_list #> apsnd (map_filter I 

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

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

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

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

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

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

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

828 
add_datatypes stmts 

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

830 
add_datatypes stmts 

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

832 
add_class stmts 

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

834 
add_class stmts 

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

836 
add_class stmts 

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

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

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

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

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

843 
fun add_stmts' stmts nsp_nodes = 

844 
let 

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

846 
val deps = 

847 
[] 

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

849 
> subtract (op =) names; 

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

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

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

854 
^ commas (map labelled_name names) 

855 
^ "\n" 

856 
^ commas module_names); 

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

857 
val module_name_path = Long_Name.explode module_name; 
28054  858 
fun add_dep name name' = 
859 
let 

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

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

863 
else let 

28705  864 
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

865 
(module_name_path, Long_Name.explode module_name'); 
28054  866 
in 
867 
map_node common 

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

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

870 
^ quote name ^ " > " ^ quote name' 

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

872 
end end; 

873 
in 

874 
nsp_nodes 

875 
> map_nsp_yield module_name_path (add_stmts stmts) 

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

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

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

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

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

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

882 
end; 

883 
val (_, nodes) = empty_module 

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

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

886 
fun deresolver prefix name = 

887 
let 

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

888 
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

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

892 
nodes 

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

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

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

896 
 Dummy stmt_name => stmt_name); 

897 
in 

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

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

901 
in (deresolver, nodes) end; 

902 

33992  903 
fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name 
34071  904 
reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination = 
28054  905 
let 
906 
val is_cons = Code_Thingol.is_cons program; 

33992  907 
val presentation_stmt_names = Code_Target.stmt_names_of_destination destination; 
908 
val is_presentation = not (null presentation_stmt_names); 

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

28054  910 
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

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

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

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

920 
let 

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

922 
val p = if is_presentation then Pretty.chunks2 body 

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

924 
in SOME ([], p) end 

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

926 
o rev o flat o Graph.strong_conn) nodes 

927 
> split_list 

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

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

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

34071  934 
(case compile of SOME compile => SOME (compile o code_of_pretty)  NONE => NONE) 
935 
(fn NONE => code_writeln  SOME file => File.write file o code_of_pretty) 

936 
(rpair stmt_names' o code_of_pretty) p destination 

28054  937 
end; 
938 

939 
end; (*local*) 

940 

941 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

942 
(** for instrumentalization **) 
28054  943 

34032  944 
fun evaluation_code_of thy target struct_name = 
945 
Code_Target.serialize_custom thy (target, (fn _ => fn [] => 

946 
serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml)); 

28054  947 

948 

949 
(** Isar setup **) 

950 

951 
fun isar_seri_sml module_name = 

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

31327  954 
(SOME (use_text ML_Env.local_context (1, "generated code") false)) 
33992  955 
print_sml_module print_sml_stmt module_name with_signatures)); 
28054  956 

957 
fun isar_seri_ocaml module_name = 

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

960 
print_ocaml_module print_ocaml_stmt module_name with_signatures)); 

28054  961 

962 
val setup = 

28064  963 
Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml)) 
964 
#> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml)) 

33992  965 
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36536
diff
changeset

966 
brackify_infix (1, R) fxy ( 
33992  967 
print_typ (INFX (1, X)) ty1, 
28054  968 
str ">", 
33992  969 
print_typ (INFX (1, R)) ty2 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36536
diff
changeset

970 
))) 
33992  971 
#> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36536
diff
changeset

972 
brackify_infix (1, R) fxy ( 
33992  973 
print_typ (INFX (1, X)) ty1, 
28054  974 
str ">", 
33992  975 
print_typ (INFX (1, R)) ty2 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36536
diff
changeset

976 
))) 
28054  977 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
978 
#> fold (Code_Target.add_reserved target_SML) 

34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

979 
["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"] 
28054  980 
#> fold (Code_Target.add_reserved target_OCaml) [ 
981 
"and", "as", "assert", "begin", "class", 

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

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

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

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

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

987 
"virtual", "when", "while", "with" 

988 
] 

34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

989 
#> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]; 
28054  990 

991 
end; (*struct*) 