author  bulwahn 
Mon, 02 May 2011 10:50:09 +0200  
changeset 42599  1a82b0400b2a 
parent 41952  c7297638599b 
child 43326  47cf4bc789aa 
child 43343  e83695ea0e0a 
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); 

41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

79 
fun print_classrels fxy [] ps = brackify fxy ps 
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

80 
 print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps] 
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

81 
 print_classrels fxy classrels ps = 
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

82 
brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps] 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

83 
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

84 
print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x) 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

85 
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

86 
((str o deresolve) inst :: 
33992  87 
(if is_pseudo_fun inst then [str "()"] 
88 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

89 
 print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

90 
[str (if k = 1 then first_upper v ^ "_" 
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

91 
else first_upper v ^ string_of_int (i+1) ^ "_")] 
38922  92 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  93 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

94 
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort)); 
35228  95 
fun print_term is_pseudo_fun some_thm vars fxy (IConst c) = 
96 
print_app is_pseudo_fun some_thm vars fxy (c, []) 

97 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

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

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

105 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

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

119 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

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

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

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

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

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

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

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

148 
str "end" 
28054  149 
] 
150 
end 

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

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

28054  165 
) 
166 
end 

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

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

172 
let 

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

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

178 
str definer 

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

180 
:: str "=" 

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

182 
) 

183 
end; 

184 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

210 
in pair 

211 
(print_val_decl print_typscheme (name, vs_ty)) 

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

213 
print_eqn definer eq 

214 
:: map (print_eqn "") eqs 

215 
)) 

29189  216 
end 
33992  217 
 print_def is_pseudo_fun _ definer 
37449  218 
(ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) = 
29189  219 
let 
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

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

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

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

223 
str "=", 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

224 
print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

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

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

231 
]; 
33992  232 
in pair 
233 
(print_val_decl print_dicttypscheme 

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

235 
(concat ( 

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

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

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

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

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

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

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

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

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

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

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

250 
((semicolon o map str) ( 

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

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

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

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

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

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

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

259 
 print_stmt (ML_Val binding) = 

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

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

263 
[sig_p] 

264 
(semicolon [p]) 

265 
end 

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

267 
let 

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

269 
fun print_pseudo_fun name = concat [ 

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

272 
str "=", 

273 
(str o deresolve) name, 

274 
str "();" 

275 
]; 

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

278 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

279 
in pair 

280 
sig_ps 

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

282 
end 

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

284 
let 

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

286 
in 

287 
pair 

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

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

290 
end 

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

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

295 
val (ps, p) = split_last sig_ps; 

296 
in pair 

297 
sig_ps 

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

299 
end 

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

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

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

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

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

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

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

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

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

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

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

316 
fun print_classparam_field (classparam, ty) = 

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

318 
fun print_classparam_proj (classparam, ty) = 

319 
print_proj (deresolve classparam) 

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

321 
in pair 

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

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

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

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

328 
(str o deresolve) class, 

329 
str "=", 

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

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

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

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

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

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

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

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

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

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

348 
:: body 

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

28054  350 
); 
351 

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

354 
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

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

356 
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

357 
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

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

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

362 

28054  363 

364 
(** OCaml serializer **) 

365 

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

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

371 
 print_tyco_expr fxy (tyco, tys) = 

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

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

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

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

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

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

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

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

41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

383 
val print_classrels = 
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

384 
fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel]) 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

385 
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

386 
print_plain_dict is_pseudo_fun fxy x 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

387 
> print_classrels classrels 
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

388 
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = 
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

389 
brackify BR ((str o deresolve) inst :: 
33992  390 
(if is_pseudo_fun inst then [str "()"] 
391 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

392 
 print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = 
33992  393 
str (if k = 1 then "_" ^ first_upper v 
394 
else "_" ^ first_upper v ^ string_of_int (i+1)) 

38922  395 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  396 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

397 
(map_index (fn (i, _) => Dict ([], Dict_Var (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 
38923  416 
of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax 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 

38922  425 
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) 
35228  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) 

38923  433 
(print_term is_pseudo_fun) const_syntax 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 

37449  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 
42599
1a82b0400b2a
improving naming of fresh variables in OCaml serializer
bulwahn
parents:
41952
diff
changeset

486 
> intro_base_names 
1a82b0400b2a
improving naming of fresh variables in OCaml serializer
bulwahn
parents:
41952
diff
changeset

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

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

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

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

500 
> intro_base_names 
38923  501 
(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

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

505 
concat ( 

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

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

515 
:: Pretty.brk 1 

516 
:: str "function" 

517 
:: Pretty.brk 1 

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

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

526 
> intro_base_names 
38923  527 
(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

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

531 
Pretty.breaks dummy_parms 

532 
@ Pretty.brk 1 

533 
:: str "=" 

534 
:: Pretty.brk 1 

535 
:: str "match" 

536 
:: Pretty.brk 1 

38778  537 
:: (Pretty.block o commas) dummy_parms 
28054  538 
:: Pretty.brk 1 
539 
:: str "with" 

540 
:: Pretty.brk 1 

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

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

546 
val prolog = if needs_typ then 
33992  547 
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

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

551 
(concat ( 

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

552 
prolog 
33992  553 
:: print_dict_args vs 
554 
@ print_eqns (is_pseudo_fun name) eqs 

555 
)) 

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

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

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

559 
let 
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

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

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

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

563 
str "=", 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

564 
print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

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

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

571 
]; 
33992  572 
in pair 
573 
(print_val_decl print_dicttypscheme 

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

575 
(concat ( 

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

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

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

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

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

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

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

583 
str ":", 
33992  584 
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

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

587 
end; 
33992  588 
fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair 
589 
[print_val_decl print_typscheme (name, vs_ty)] 

590 
((doublesemicolon o map str) ( 

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

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

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

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

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

595 
:: "failwith" 
33992  596 
@@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name 
597 
)) 

598 
 print_stmt (ML_Val binding) = 

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

599 
let 
33992  600 
val (sig_p, p) = print_def (K false) true "let" binding 
601 
in pair 

602 
[sig_p] 

603 
(doublesemicolon [p]) 

604 
end 

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

606 
let 

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

608 
fun print_pseudo_fun name = concat [ 

29189  609 
str "let", 
610 
(str o deresolve) name, 

611 
str "=", 

612 
(str o deresolve) name, 

613 
str "();;" 

614 
]; 

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

617 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

618 
in pair 

619 
sig_ps 

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

621 
end 

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

623 
let 

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

625 
in 

626 
pair 

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

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

629 
end 

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

28054  631 
let 
33992  632 
val sig_ps = print_datatype_decl "type" data 
633 
:: map (print_datatype_decl "and") datas; 

634 
val (ps, p) = split_last sig_ps; 

635 
in pair 

636 
sig_ps 

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

638 
end 

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

639 
 print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = 
28054  640 
let 
33992  641 
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

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

643 
print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v)); 
33992  644 
fun print_classparam_decl (classparam, ty) = 
645 
print_val_decl print_typscheme 

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

647 
fun print_classparam_field (classparam, ty) = 

648 
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

649 
val w = "_" ^ first_upper v; 
33992  650 
fun print_classparam_proj (classparam, _) = 
651 
(concat o map str) ["let", deresolve classparam, w, "=", 

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

653 
val type_decl_p = concat [ 

654 
str ("type '" ^ v), 

655 
(str o deresolve) class, 

28054  656 
str "=", 
33992  657 
enum_default "unit" ";" "{" "}" ( 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

658 
map print_super_class_field super_classes 
33992  659 
@ map print_classparam_field classparams 
660 
) 

28054  661 
]; 
33992  662 
in pair 
663 
(type_decl_p :: map print_classparam_decl classparams) 

664 
(Pretty.chunks ( 

665 
doublesemicolon [type_decl_p] 

666 
:: map print_classparam_proj classparams 

667 
)) 

668 
end; 

669 
in print_stmt end; 

28054  670 

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

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

672 
Pretty.chunks2 ( 
33992  673 
Pretty.chunks ( 
674 
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

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

678 
:: body 

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

28054  680 
); 
681 

28064  682 
val literals_ocaml = let 
683 
fun chr i = 

684 
let 

685 
val xs = string_of_int i; 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
39148
diff
changeset

686 
val ys = replicate_string (3  length (raw_explode xs)) "0"; 
28064  687 
in "\\" ^ ys ^ xs end; 
688 
fun char_ocaml c = 

689 
let 

690 
val i = ord c; 

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

692 
then chr i else c 

693 
in s end; 

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

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

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

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

697 
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

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

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

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

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

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

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

706 
literal_list = enum ";" "[" "]", 
28064  707 
infix_cons = (6, "::") 
708 
} end; 

709 

710 

28054  711 

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

713 

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

714 
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

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

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

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

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

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

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_type base (nsp_const, nsp_type) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

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

723 
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

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

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

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

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

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

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

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

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

732 
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

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

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

735 
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

736 
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

737 
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

738 
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

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

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

741 
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

742 
 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

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

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

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

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

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

748 
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

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

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

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

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

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

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

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

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

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

760 
fun modify_datatypes stmts = single (SOME 

761 
(ML_Datas (map_filter 

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

763 
fun modify_class stmts = single (SOME 

764 
(ML_Class (the_single (map_filter 

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

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

767 
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

768 
 modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = 
39061  769 
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

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

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

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

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

774 
 modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) = 
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 ((stmts as (_, Code_Thingol.Classrel _)::_)) = 
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

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

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

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

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

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

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

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

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

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

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

787 
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

788 
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

789 
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

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

791 

39148  792 
fun serialize_ml target print_ml_module print_ml_stmt with_signatures 
39142  793 
{ labelled_name, reserved_syms, includes, module_alias, 
41343  794 
class_syntax, tyco_syntax, const_syntax } program = 
28054  795 
let 
39147  796 

797 
(* build program *) 

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

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

799 
ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program; 
39147  800 

801 
(* print statements *) 

802 
fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt 

803 
labelled_name tyco_syntax const_syntax (make_vars reserved_syms) 

804 
(Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt 

805 
> apfst SOME; 

806 

807 
(* print modules *) 

808 
fun print_module prefix_fragments base _ xs = 

809 
let 

810 
val (raw_decls, body) = split_list xs; 

811 
val decls = if with_signatures then SOME (maps these raw_decls) else NONE 

812 
in (NONE, print_ml_module base decls body) end; 

813 

814 
(* serialization *) 

815 
val p = Pretty.chunks2 (map snd includes 

816 
@ map snd (Code_Namespace.print_hierarchical { 

817 
print_module = print_module, print_stmt = print_stmt, 

818 
lift_markup = apsnd } ml_program)); 

39056  819 
fun write width NONE = writeln o format [] width 
820 
 write width (SOME p) = File.write p o format [] width; 

28054  821 
in 
39102  822 
Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p 
28054  823 
end; 
824 

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

38924  828 
print_sml_module print_sml_stmt with_signatures)); 
28054  829 

38966  830 
val serializer_ocaml : Code_Target.serializer = 
33992  831 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
37748  832 
>> (fn with_signatures => serialize_ml target_OCaml 
38924  833 
print_ocaml_module print_ocaml_stmt with_signatures)); 
28054  834 

38966  835 

836 
(** Isar setup **) 

837 

28054  838 
val setup = 
37821  839 
Code_Target.add_target 
38966  840 
(target_SML, { serializer = serializer_sml, literals = literals_sml, 
41940  841 
check = { env_var = "ISABELLE_PROCESS", 
842 
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), 

843 
make_command = fn _ => "\"$ISABELLE_PROCESS\" r q u Pure" } }) 

37821  844 
#> Code_Target.add_target 
38966  845 
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, 
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP  discontinued implicit detection;
wenzelm
parents:
41940
diff
changeset

846 
check = { env_var = "ISABELLE_OCAML", 
41940  847 
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), 
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP  discontinued implicit detection;
wenzelm
parents:
41940
diff
changeset

848 
make_command = fn _ => "\"$ISABELLE_OCAML\" w pu nums.cma ROOT.ocaml" } }) 
38923  849 
#> 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

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

854 
))) 
38923  855 
#> 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

856 
brackify_infix (1, R) fxy ( 
33992  857 
print_typ (INFX (1, X)) ty1, 
28054  858 
str ">", 
33992  859 
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

860 
))) 
28054  861 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
862 
#> fold (Code_Target.add_reserved target_SML) 

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

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

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

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

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

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

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

872 
"virtual", "when", "while", "with" 

873 
] 

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

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

876 
end; (*struct*) 