author  haftmann 
Thu, 02 Sep 2010 19:08:48 +0200  
changeset 39102  4ae1d212100f 
parent 39061  9b1fd2df743c 
child 39142  f63715f00fdd 
child 39147  3c284a152bd6 
permissions  rwrr 
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37449
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 

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

9 
val target_SML: string 
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37449
diff
changeset

10 
val target_OCaml: string 
28054  11 
val setup: theory > theory 
12 
end; 

13 

14 
structure Code_ML : CODE_ML = 

15 
struct 

16 

17 
open Basic_Code_Thingol; 

18 
open Code_Printer; 

19 

20 
infixr 5 @@; 

21 
infixr 5 @; 

22 

33992  23 

24 
(** generic **) 

25 

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

28 

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

29 
datatype ml_binding = 
35228  30 
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

31 
 ML_Instance of string * ((class * (string * (vname * sort) list)) 
37445
e372fa3c7239
dropped obscure type argument weakening mapping  was only a misunderstanding
haftmann
parents:
37439
diff
changeset

32 
* ((class * (string * (string * dict list list))) list 
37449  33 
* (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list))); 
28054  34 

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

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

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

38 
 ML_Funs of ml_binding list * string list 
37449  39 
 ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list 
37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset

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

41 

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

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

43 
 stmt_name_of_binding (ML_Instance (name, _)) = name; 
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_names_of (ML_Exc (name, _)) = [name] 
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

47 
 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

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

49 
 stmt_names_of (ML_Class (name, _)) = [name]; 
28054  50 

33992  51 
fun print_product _ [] = NONE 
52 
 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

53 
 print_product print xs = (SOME o enum " *" "" "") (map print xs); 
28054  54 

38922  55 
fun tuplify _ _ [] = NONE 
56 
 tuplify print fxy [x] = SOME (print fxy x) 

57 
 tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); 

28054  58 

33992  59 

60 
(** SML serializer **) 

61 

38923  62 
fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve = 
28054  63 
let 
33992  64 
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco 
65 
 print_tyco_expr fxy (tyco, [ty]) = 

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

67 
 print_tyco_expr fxy (tyco, tys) = 

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

68 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 
38923  69 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
33992  70 
of NONE => print_tyco_expr fxy (tyco, tys) 
71 
 SOME (i, print) => print print_typ fxy tys) 

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

73 
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

74 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  75 
(map_filter (fn (v, sort) => 
76 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

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

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

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

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

82 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

84 
let 

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

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

87 
in case classrels 

88 
of [] => v_p 

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

90 
 classrels => brackets 

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

91 
[enum " o" "(" ")" (map (str o deresolve) classrels), v_p] 
33992  92 
end 
38922  93 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  94 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 
95 
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); 

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

98 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  99 
str "_" 
35228  100 
 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

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

106 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

28054  116 
(case Code_Thingol.unfold_const_app t0 
38923  117 
of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) 
35228  118 
then print_case is_pseudo_fun some_thm vars fxy cases 
119 
else print_app is_pseudo_fun some_thm vars fxy c_ts 

120 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

37449  121 
and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) = 
29175  122 
if is_cons c then 
37449  123 
let val k = length function_typs in 
33992  124 
if k < 2 orelse length ts = k 
125 
then (str o deresolve) c 

38922  126 
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) 
35228  127 
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] 
33992  128 
end 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

147 
Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], 
35228  148 
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

149 
str "end" 
28054  150 
] 
151 
end 

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

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

28054  166 
) 
167 
end 

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

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

173 
let 

37449  174 
fun print_co ((co, _), []) = str (deresolve co) 
175 
 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

176 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  177 
in 
178 
concat ( 

179 
str definer 

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

181 
:: str "=" 

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

183 
) 

184 
end; 

185 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

192 
> intro_base_names 
38923  193 
(is_none o const_syntax) deresolve consts 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

196 
val prolog = if needs_typ then 
33992  197 
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

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

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

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

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

202 
:: (if is_pseudo_fun name then [str "()"] 
33992  203 
else print_dict_args vs 
35228  204 
@ 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

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

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

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

211 
in pair 

212 
(print_val_decl print_typscheme (name, vs_ty)) 

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

214 
print_eqn definer eq 

215 
:: map (print_eqn "") eqs 

216 
)) 

29189  217 
end 
33992  218 
 print_def is_pseudo_fun _ definer 
37449  219 
(ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) = 
29189  220 
let 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

221 
fun print_super_instance (_, (classrel, dss)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

226 
]; 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

227 
fun print_classparam_instance ((classparam, const), (thm, _)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

230 
str "=", 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

231 
print_app (K false) (SOME thm) reserved NOBR (const, []) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

232 
]; 
33992  233 
in pair 
234 
(print_val_decl print_dicttypscheme 

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

236 
(concat ( 

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

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

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

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

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

242 
:: enum "," "{" "}" 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

243 
(map print_super_instance super_instances 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

244 
@ map print_classparam_instance classparam_instances) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

251 
((semicolon o map str) ( 

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

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

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

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

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

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

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

260 
 print_stmt (ML_Val binding) = 

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

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

264 
[sig_p] 

265 
(semicolon [p]) 

266 
end 

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

268 
let 

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

270 
fun print_pseudo_fun name = concat [ 

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

273 
str "=", 

274 
(str o deresolve) name, 

275 
str "();" 

276 
]; 

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

279 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

280 
in pair 

281 
sig_ps 

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

283 
end 

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

285 
let 

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

287 
in 

288 
pair 

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

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

291 
end 

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

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

296 
val (ps, p) = split_last sig_ps; 

297 
in pair 

298 
sig_ps 

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

300 
end 

37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset

301 
 print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = 
28054  302 
let 
33992  303 
fun print_field s p = concat [str s, str ":", p]; 
304 
fun print_proj s p = semicolon 

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

37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

306 
fun print_super_class_decl (super_class, classrel) = 
33992  307 
print_val_decl print_dicttypscheme 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

308 
(classrel, ([(v, [class])], (super_class, ITyVar v))); 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

309 
fun print_super_class_field (super_class, classrel) = 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

310 
print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v)); 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

311 
fun print_super_class_proj (super_class, classrel) = 
33992  312 
print_proj (deresolve classrel) 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

313 
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v))); 
33992  314 
fun print_classparam_decl (classparam, ty) = 
315 
print_val_decl print_typscheme 

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

317 
fun print_classparam_field (classparam, ty) = 

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

319 
fun print_classparam_proj (classparam, ty) = 

320 
print_proj (deresolve classparam) 

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

322 
in pair 

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

37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

324 
:: map print_super_class_decl super_classes 
33992  325 
@ map print_classparam_decl classparams) 
326 
(Pretty.chunks ( 

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

329 
(str o deresolve) class, 

330 
str "=", 

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

331 
enum "," "{" "};" ( 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

332 
map print_super_class_field super_classes 
33992  333 
@ map print_classparam_field classparams 
28054  334 
) 
335 
] 

37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

336 
:: map print_super_class_proj super_classes 
33992  337 
@ map print_classparam_proj classparams 
338 
)) 

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

38933
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38928
diff
changeset

342 
fun print_sml_module name some_decls body = 
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38928
diff
changeset

343 
Pretty.chunks2 ( 
33992  344 
Pretty.chunks ( 
345 
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

346 
:: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls 
33992  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, 

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

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

357 
literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)", 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37822
diff
changeset

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

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

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

363 

28054  364 

365 
(** OCaml serializer **) 

366 

38923  367 
fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve = 
28054  368 
let 
33992  369 
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco 
370 
 print_tyco_expr fxy (tyco, [ty]) = 

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

372 
 print_tyco_expr fxy (tyco, tys) = 

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

373 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 
38923  374 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
33992  375 
of NONE => print_tyco_expr fxy (tyco, tys) 
376 
 SOME (i, print) => print print_typ fxy tys) 

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

378 
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

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

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

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

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

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

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

387 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

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

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

391 
> fold_rev (fn classrel => fn p => 

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

38922  393 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  394 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 
395 
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); 

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

398 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  399 
str "_" 
35228  400 
 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

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

406 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

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

33992  413 
(case Code_Thingol.unfold_const_app t0 
38923  414 
of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) 
35228  415 
then print_case is_pseudo_fun some_thm vars fxy cases 
416 
else print_app is_pseudo_fun some_thm vars fxy c_ts 

417 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

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

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

422 
then (str o deresolve) c 

38922  423 
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) 
35228  424 
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] 
33992  425 
end 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

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

28054  458 
) 
459 
end 

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

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

465 
let 

37449  466 
fun print_co ((co, _), []) = str (deresolve co) 
467 
 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

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

471 
str definer 

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

473 
:: str "=" 

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

475 
) 

476 
end; 

477 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

501 
concat ( 

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

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

511 
:: Pretty.brk 1 

512 
:: str "function" 

513 
:: Pretty.brk 1 

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

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

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

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

527 
Pretty.breaks dummy_parms 

528 
@ Pretty.brk 1 

529 
:: str "=" 

530 
:: Pretty.brk 1 

531 
:: str "match" 

532 
:: Pretty.brk 1 

38778  533 
:: (Pretty.block o commas) dummy_parms 
28054  534 
:: Pretty.brk 1 
535 
:: str "with" 

536 
:: Pretty.brk 1 

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

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

542 
val prolog = if needs_typ then 
33992  543 
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

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

547 
(concat ( 

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

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

551 
)) 

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

552 
end 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

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

555 
let 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

556 
fun print_super_instance (_, (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 
]; 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

562 
fun print_classparam_instance ((classparam, const), (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 "=", 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

566 
print_app (K false) (SOME thm) reserved NOBR (const, []) 
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 [ 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

577 
enum_default "()" ";" "{" "}" (map print_super_instance super_instances 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

578 
@ map print_classparam_instance classparam_instances), 
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 

37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset

635 
 print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = 
28054  636 
let 
33992  637 
fun print_field s p = concat [str s, str ":", p]; 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

638 
fun print_super_class_field (super_class, classrel) = 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

639 
print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v)); 
33992  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" ";" "{" "}" ( 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

654 
map print_super_class_field super_classes 
33992  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 

38933
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38928
diff
changeset

667 
fun print_ocaml_module name some_decls body = 
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38928
diff
changeset

668 
Pretty.chunks2 ( 
33992  669 
Pretty.chunks ( 
670 
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

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

674 
:: body 

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

28054  676 
); 
677 

28064  678 
val literals_ocaml = let 
679 
fun chr i = 

680 
let 

681 
val xs = string_of_int i; 

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

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

684 
fun char_ocaml c = 

685 
let 

686 
val i = ord c; 

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

688 
then chr i else c 

689 
in s end; 

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

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

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

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

693 
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

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

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

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

699 
literal_positive_numeral = numeral_ocaml, 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37822
diff
changeset

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

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

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

705 

706 

28054  707 

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

709 

39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

710 
fun ml_program_of_program labelled_name reserved module_alias program = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

711 
let 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

712 
fun namify_const upper base (nsp_const, nsp_type) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

713 
let 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

714 
val (base', nsp_const') = yield_singleton Name.variants 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

715 
(if upper then first_upper base else base) nsp_const 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

716 
in (base', (nsp_const', nsp_type)) end; 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

717 
fun namify_type base (nsp_const, nsp_type) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

718 
let 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

719 
val (base', nsp_type') = yield_singleton Name.variants base nsp_type 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

720 
in (base', (nsp_const, nsp_type')) end; 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

721 
fun namify_stmt (Code_Thingol.Fun _) = namify_const false 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

722 
 namify_stmt (Code_Thingol.Datatype _) = namify_type 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

723 
 namify_stmt (Code_Thingol.Datatypecons _) = namify_const true 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

724 
 namify_stmt (Code_Thingol.Class _) = namify_type 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

725 
 namify_stmt (Code_Thingol.Classrel _) = namify_const false 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

726 
 namify_stmt (Code_Thingol.Classparam _) = namify_const false 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

727 
 namify_stmt (Code_Thingol.Classinst _) = namify_const false; 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

728 
fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

729 
let 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

730 
val eqs = filter (snd o snd) raw_eqs; 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

731 
val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

732 
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

733 
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

734 
else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

735 
 _ => (eqs, NONE) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

736 
else (eqs, NONE) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

737 
in (ML_Function (name, (tysm, eqs')), some_value_name) end 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

738 
 ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

739 
(ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

740 
 ml_binding_of_stmt (name, _) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

741 
error ("Binding block containing illegal statement: " ^ labelled_name name) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

742 
fun modify_fun (name, stmt) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

743 
let 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

744 
val (binding, some_value_name) = ml_binding_of_stmt (name, stmt); 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

745 
val ml_stmt = case binding 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

746 
of ML_Function (name, ((vs, ty), [])) => 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

747 
ML_Exc (name, ((vs, ty), 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

748 
(length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

749 
 _ => case some_value_name 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

750 
of NONE => ML_Funs ([binding], []) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

751 
 SOME (name, true) => ML_Funs ([binding], [name]) 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

752 
 SOME (name, false) => ML_Val binding 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

753 
in SOME ml_stmt end; 
39031  754 
fun modify_funs stmts = single (SOME 
755 
(ML_Funs (map_split ml_binding_of_stmt stmts > (apsnd o map_filter o Option.map) fst))) 

756 
fun modify_datatypes stmts = single (SOME 

757 
(ML_Datas (map_filter 

758 
(fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt)  _ => NONE) stmts))) 

759 
fun modify_class stmts = single (SOME 

760 
(ML_Class (the_single (map_filter 

761 
(fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt)  _ => NONE) stmts)))) 

39059
3a11a667af75
restored and added surpression of case combinators
haftmann
parents:
39058
diff
changeset

762 
fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) = 
3a11a667af75
restored and added surpression of case combinators
haftmann
parents:
39058
diff
changeset

763 
if Code_Thingol.is_case stmt' then [] else [modify_fun stmt] 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

764 
 modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = 
39061  765 
modify_funs (filter_out (Code_Thingol.is_case o snd) stmts) 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

766 
 modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

767 
modify_datatypes stmts 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

768 
 modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

769 
modify_datatypes stmts 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

770 
 modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

771 
modify_class stmts 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

772 
 modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

773 
modify_class stmts 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

774 
 modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

775 
modify_class stmts 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

776 
 modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

777 
[modify_fun stmt] 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

778 
 modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

779 
modify_funs stmts 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

780 
 modify_stmts stmts = error ("Illegal mutual dependencies: " ^ 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

781 
(Library.commas o map (labelled_name o fst)) stmts); 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

782 
in 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

783 
Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved, 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

784 
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt, 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

785 
cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

786 
end; 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

787 

38926  788 
fun serialize_ml target print_module print_stmt with_signatures { labelled_name, 
38928  789 
reserved_syms, includes, module_alias, class_syntax, tyco_syntax, 
39058  790 
const_syntax, program, names } = 
28054  791 
let 
792 
val is_cons = Code_Thingol.is_cons program; 

39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

793 
val { deresolver, hierarchical_program = ml_program } = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

794 
ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program; 
39056  795 
val print_stmt = print_stmt labelled_name tyco_syntax const_syntax 
796 
(make_vars reserved_syms) is_cons; 

39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

797 
fun print_node _ (_, Code_Namespace.Dummy) = 
28054  798 
NONE 
39056  799 
 print_node prefix_fragments (name, Code_Namespace.Stmt stmt) = 
39057
c6d146ed07ae
manage statement selection for presentation wholly through markup
haftmann
parents:
39056
diff
changeset

800 
SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt)) 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

801 
 print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) = 
33992  802 
let 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

803 
val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes; 
39057
c6d146ed07ae
manage statement selection for presentation wholly through markup
haftmann
parents:
39056
diff
changeset

804 
val p = print_module name_fragment 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

805 
(if with_signatures then SOME decls else NONE) body; 
33992  806 
in SOME ([], p) end 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

807 
and print_nodes prefix_fragments nodes = (map_filter 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

808 
(fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name))) 
33992  809 
o rev o flat o Graph.strong_conn) nodes 
810 
> split_list 

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

39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

812 
val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program)); 
39056  813 
fun write width NONE = writeln o format [] width 
814 
 write width (SOME p) = File.write p o format [] width; 

28054  815 
in 
39102  816 
Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p 
28054  817 
end; 
818 

38966  819 
val serializer_sml : Code_Target.serializer = 
33992  820 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
821 
>> (fn with_signatures => serialize_ml target_SML 

38924  822 
print_sml_module print_sml_stmt with_signatures)); 
28054  823 

38966  824 
val serializer_ocaml : Code_Target.serializer = 
33992  825 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
37748  826 
>> (fn with_signatures => serialize_ml target_OCaml 
38924  827 
print_ocaml_module print_ocaml_stmt with_signatures)); 
28054  828 

38966  829 

830 
(** Isar setup **) 

831 

28054  832 
val setup = 
37821  833 
Code_Target.add_target 
38966  834 
(target_SML, { serializer = serializer_sml, literals = literals_sml, 
37822
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

835 
check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), 
38863
9070a7c356c9
code checking: compiler invocation happens in same directory as generated file  avoid problem with different path representations on cygwin
haftmann
parents:
38784
diff
changeset

836 
make_command = fn isabelle => fn _ => isabelle ^ " r q u Pure" } }) 
37821  837 
#> Code_Target.add_target 
38966  838 
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, 
37822
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

839 
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), 
38863
9070a7c356c9
code checking: compiler invocation happens in same directory as generated file  avoid problem with different path representations on cygwin
haftmann
parents:
38784
diff
changeset

840 
make_command = fn ocaml => fn _ => ocaml ^ " w pu nums.cma ROOT.ocaml" } }) 
38923  841 
#> Code_Target.add_tyco_syntax 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

842 
brackify_infix (1, R) fxy ( 
33992  843 
print_typ (INFX (1, X)) ty1, 
28054  844 
str ">", 
33992  845 
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

846 
))) 
38923  847 
#> Code_Target.add_tyco_syntax 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

848 
brackify_infix (1, R) fxy ( 
33992  849 
print_typ (INFX (1, X)) ty1, 
28054  850 
str ">", 
33992  851 
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

852 
))) 
28054  853 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
854 
#> fold (Code_Target.add_reserved target_SML) 

38070  855 
["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*), 
856 
"Fail", "div", "mod" (*standard infixes*), "IntInf"] 

28054  857 
#> fold (Code_Target.add_reserved target_OCaml) [ 
858 
"and", "as", "assert", "begin", "class", 

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

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

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

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

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

864 
"virtual", "when", "while", "with" 

865 
] 

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

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

868 
end; (*struct*) 