author  haftmann 
Mon, 30 Aug 2010 09:28:02 +0200  
changeset 38863  9070a7c356c9 
parent 38784  3b4d63ab03c4 
child 38910  6af1d8673cbf 
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 
34032  11 
val evaluation_code_of: theory > string > string 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

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

28054  15 
val setup: theory > theory 
16 
end; 

17 

18 
structure Code_ML : CODE_ML = 

19 
struct 

20 

21 
open Basic_Code_Thingol; 

22 
open Code_Printer; 

23 

24 
infixr 5 @@; 

25 
infixr 5 @; 

26 

33992  27 

28 
(** generic **) 

29 

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

32 

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

33 
datatype ml_binding = 
35228  34 
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

35 
 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

36 
* ((class * (string * (string * dict list list))) list 
37449  37 
* (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list))); 
28054  38 

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

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

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

42 
 ML_Funs of ml_binding list * string list 
37449  43 
 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

44 
 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

45 

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

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

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

48 

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

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

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

51 
 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

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

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

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

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

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

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

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

33992  63 

64 
(** SML serializer **) 

65 

66 
fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = 

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

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

71 
 print_tyco_expr fxy (tyco, tys) = 

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

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

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

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

77 
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

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

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

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

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

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

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

86 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

88 
let 

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

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

91 
in case classrels 

92 
of [] => v_p 

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

94 
 classrels => brackets 

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

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

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

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

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

102 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  103 
str "_" 
35228  104 
 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

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

110 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

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

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

124 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

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

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

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

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

138 
(print_term is_pseudo_fun) syntax_const some_thm vars 

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

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

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

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

153 
str "end" 
28054  154 
] 
155 
end 

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

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

28054  170 
) 
171 
end 

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

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

177 
let 

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

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

183 
str definer 

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

185 
:: str "=" 

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

187 
) 

188 
end; 

189 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

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

200 
val prolog = if needs_typ then 
33992  201 
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

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

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

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

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

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

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

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

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

215 
in pair 

216 
(print_val_decl print_typscheme (name, vs_ty)) 

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

218 
print_eqn definer eq 

219 
:: map (print_eqn "") eqs 

220 
)) 

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

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

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

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

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

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

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

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

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

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

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

236 
]; 
33992  237 
in pair 
238 
(print_val_decl print_dicttypscheme 

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

240 
(concat ( 

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

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

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

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

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

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

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

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

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

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

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

255 
((semicolon o map str) ( 

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

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

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

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

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

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

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

264 
 print_stmt (ML_Val binding) = 

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

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

268 
[sig_p] 

269 
(semicolon [p]) 

270 
end 

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

272 
let 

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

274 
fun print_pseudo_fun name = concat [ 

29189  275 
str "val", 
276 
(str o deresolve) name, 

277 
str "=", 

278 
(str o deresolve) name, 

279 
str "();" 

280 
]; 

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

283 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

284 
in pair 

285 
sig_ps 

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

287 
end 

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

289 
let 

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

291 
in 

292 
pair 

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

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

295 
end 

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

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

300 
val (ps, p) = split_last sig_ps; 

301 
in pair 

302 
sig_ps 

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

304 
end 

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

305 
 print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = 
28054  306 
let 
33992  307 
fun print_field s p = concat [str s, str ":", p]; 
308 
fun print_proj s p = semicolon 

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

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

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

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

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

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

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

317 
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v))); 
33992  318 
fun print_classparam_decl (classparam, ty) = 
319 
print_val_decl print_typscheme 

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

321 
fun print_classparam_field (classparam, ty) = 

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

323 
fun print_classparam_proj (classparam, ty) = 

324 
print_proj (deresolve classparam) 

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

326 
in pair 

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

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

328 
:: map print_super_class_decl super_classes 
33992  329 
@ map print_classparam_decl classparams) 
330 
(Pretty.chunks ( 

28054  331 
concat [ 
332 
str ("type '" ^ v), 

333 
(str o deresolve) class, 

334 
str "=", 

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

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

336 
map print_super_class_field super_classes 
33992  337 
@ map print_classparam_field classparams 
28054  338 
) 
339 
] 

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

340 
:: map print_super_class_proj super_classes 
33992  341 
@ map print_classparam_proj classparams 
342 
)) 

28054  343 
end; 
33992  344 
in print_stmt end; 
28054  345 

34032  346 
fun print_sml_module name some_decls body = if name = "" 
347 
then Pretty.chunks2 body 

348 
else Pretty.chunks2 ( 

33992  349 
Pretty.chunks ( 
350 
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

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

354 
:: body 

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

28054  356 
); 
357 

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

360 
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

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

362 
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

363 
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

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

365 
literal_list = enum "," "[" "]", 
28064  366 
infix_cons = (7, "::") 
367 
}; 

368 

28054  369 

370 
(** OCaml serializer **) 

371 

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

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

377 
 print_tyco_expr fxy (tyco, tys) = 

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

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

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

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

383 
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

384 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  385 
(map_filter (fn (v, sort) => 
386 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

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

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

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

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

392 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

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

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

396 
> fold_rev (fn classrel => fn p => 

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

398 
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); 

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

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

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

403 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  404 
str "_" 
35228  405 
 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

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

411 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

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

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

422 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

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

28054  424 
if is_cons c then 
33992  425 
let val k = length tys in 
426 
if length ts = k 

427 
then (str o deresolve) c 

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

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

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

436 
(print_term is_pseudo_fun) syntax_const some_thm vars 

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

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

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

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

28054  463 
) 
464 
end 

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

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

470 
let 

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

473 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  474 
in 
475 
concat ( 

476 
str definer 

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

478 
:: str "=" 

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

480 
) 

481 
end; 

482 
fun print_def is_pseudo_fun needs_typ definer 

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

28054  484 
let 
35228  485 
fun print_eqn ((ts, t), (some_thm, _)) = 
28054  486 
let 
32913  487 
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

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

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

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

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

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

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

506 
concat ( 

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

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

516 
:: Pretty.brk 1 

517 
:: str "function" 

518 
:: Pretty.brk 1 

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

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

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

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

532 
Pretty.breaks dummy_parms 

533 
@ Pretty.brk 1 

534 
:: str "=" 

535 
:: Pretty.brk 1 

536 
:: str "match" 

537 
:: Pretty.brk 1 

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

541 
:: Pretty.brk 1 

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

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

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

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

552 
(concat ( 

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

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

556 
)) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

572 
]; 
33992  573 
in pair 
574 
(print_val_decl print_dicttypscheme 

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

576 
(concat ( 

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

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

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

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

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

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

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

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

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

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

591 
((doublesemicolon o map str) ( 

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

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

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

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

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

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

599 
 print_stmt (ML_Val binding) = 

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

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

603 
[sig_p] 

604 
(doublesemicolon [p]) 

605 
end 

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

607 
let 

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

609 
fun print_pseudo_fun name = concat [ 

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

612 
str "=", 

613 
(str o deresolve) name, 

614 
str "();;" 

615 
]; 

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

618 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

619 
in pair 

620 
sig_ps 

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

622 
end 

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

624 
let 

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

626 
in 

627 
pair 

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

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

630 
end 

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

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

635 
val (ps, p) = split_last sig_ps; 

636 
in pair 

637 
sig_ps 

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

639 
end 

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

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

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

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

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

648 
fun print_classparam_field (classparam, ty) = 

649 
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

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

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

654 
val type_decl_p = concat [ 

655 
str ("type '" ^ v), 

656 
(str o deresolve) class, 

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

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

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

665 
(Pretty.chunks ( 

666 
doublesemicolon [type_decl_p] 

667 
:: map print_classparam_proj classparams 

668 
)) 

669 
end; 

670 
in print_stmt end; 

28054  671 

34032  672 
fun print_ocaml_module name some_decls body = if name = "" 
673 
then Pretty.chunks2 body 

674 
else Pretty.chunks2 ( 

33992  675 
Pretty.chunks ( 
676 
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

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

680 
:: body 

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

28054  682 
); 
683 

28064  684 
val literals_ocaml = let 
685 
fun chr i = 

686 
let 

687 
val xs = string_of_int i; 

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

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

690 
fun char_ocaml c = 

691 
let 

692 
val i = ord c; 

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

694 
then chr i else c 

695 
in s end; 

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

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

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

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

699 
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

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

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

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

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

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

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

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

711 

712 

28054  713 

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

715 

716 
local 

717 

718 
datatype ml_node = 

719 
Dummy of string 

720 
 Stmt of string * ml_stmt 

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

722 

723 
in 

724 

38779  725 
fun ml_node_of_program labelled_name module_name reserved module_alias program = 
28054  726 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

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

728 
val empty_module = ((reserved, reserved), Graph.empty); 
28054  729 
fun map_node [] f = f 
730 
 map_node (m::ms) f = 

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

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

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

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

735 
let 

736 
val (x, nsp') = f nsp 

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

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

739 
let 

740 
val (x, nodes') = 

741 
nodes 

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

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

744 
let 

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

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

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

748 
fun map_nsp_fun_yield f (nsp_fun, nsp_typ) = 

749 
let 

750 
val (x, nsp_fun') = f nsp_fun 

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

752 
fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = 

753 
let 

754 
val (x, nsp_typ') = f nsp_typ 

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

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

756 
val mk_name_module = mk_name_module reserved NONE module_alias program; 
28054  757 
fun mk_name_stmt upper name nsp = 
758 
let 

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

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

760 
val base' = if upper then first_upper base else base; 
28054  761 
val ([base''], nsp') = Name.variants [base'] nsp; 
762 
in (base'', nsp') end; 

37439  763 
fun deps_of names = 
764 
[] 

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

766 
> subtract (op =) names 

767 
> filter_out (Code_Thingol.is_case o Graph.get_node program); 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

803 
end; 
28054  804 
fun add_datatypes stmts = 
805 
fold_map 

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

806 
(fn (name, Code_Thingol.Datatype (_, stmt)) => 
28054  807 
map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) 
808 
 (name, Code_Thingol.Datatypecons _) => 

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

810 
 (name, _) => 

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

812 
) stmts 

813 
#>> (split_list #> apsnd (map_filter I 

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

38778  815 
^ (Library.commas o map (labelled_name o fst)) stmts) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

816 
 stmts => ML_Datas stmts))); 
28054  817 
fun add_class stmts = 
818 
fold_map 

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

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

820 
map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) 
28054  821 
 (name, Code_Thingol.Classrel _) => 
822 
map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE 

823 
 (name, Code_Thingol.Classparam _) => 

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

825 
 (name, _) => 

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

827 
) stmts 

828 
#>> (split_list #> apsnd (map_filter I 

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

38778  830 
^ (Library.commas o map (labelled_name o fst)) stmts) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

834 
 add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = 
28054  835 
add_funs stmts 
836 
 add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = 

837 
add_datatypes stmts 

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

839 
add_datatypes stmts 

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

841 
add_class stmts 

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

843 
add_class stmts 

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

845 
add_class stmts 

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

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

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

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

849 
add_funs stmts 
28054  850 
 add_stmts stmts = error ("Illegal mutual dependencies: " ^ 
38778  851 
(Library.commas o map (labelled_name o fst)) stmts); 
28054  852 
fun add_stmts' stmts nsp_nodes = 
853 
let 

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

37439  855 
val deps = deps_of names; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

856 
val (module_names, _) = (split_list o map dest_name) names; 
28054  857 
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names 
858 
handle Empty => 

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

38778  860 
^ Library.commas (map labelled_name names) 
28054  861 
^ "\n" 
38778  862 
^ Library.commas module_names); 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

863 
val module_name_path = Long_Name.explode module_name; 
28054  864 
fun add_dep name name' = 
865 
let 

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

866 
val module_name' = (mk_name_module o fst o dest_name) name'; 
28054  867 
in if module_name = module_name' then 
868 
map_node module_name_path (Graph.add_edge (name, name')) 

869 
else let 

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

871 
(module_name_path, Long_Name.explode module_name'); 
28054  872 
in 
873 
map_node common 

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

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

876 
^ quote name ^ " > " ^ quote name' 

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

878 
end end; 

879 
in 

880 
nsp_nodes 

881 
> map_nsp_yield module_name_path (add_stmts stmts) 

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

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

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

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

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

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

888 
end; 

37439  889 
val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program)) 
890 
> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt  _ => false); 

891 
val (_, nodes) = fold add_stmts' stmts empty_module; 

28054  892 
fun deresolver prefix name = 
893 
let 

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

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

895 
val module_name' = (Long_Name.explode o mk_name_module) module_name; 
28054  896 
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); 
897 
val stmt_name = 

898 
nodes 

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

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

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

902 
 Dummy stmt_name => stmt_name); 

903 
in 

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

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

907 
in (deresolver, nodes) end; 

908 

38779  909 
fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name 
910 
reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program 

911 
(stmt_names, presentation_stmt_names) = 

28054  912 
let 
913 
val is_cons = Code_Thingol.is_cons program; 

33992  914 
val is_presentation = not (null presentation_stmt_names); 
28054  915 
val (deresolver, nodes) = ml_node_of_program labelled_name module_name 
38779  916 
reserved module_alias program; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

917 
val reserved = make_vars reserved; 
33992  918 
fun print_node prefix (Dummy _) = 
28054  919 
NONE 
33992  920 
 print_node prefix (Stmt (_, stmt)) = if is_presentation andalso 
921 
(null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt 

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

925 
let 

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

927 
val p = if is_presentation then Pretty.chunks2 body 

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

929 
in SOME ([], p) end 

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

931 
o rev o flat o Graph.strong_conn) nodes 

932 
> split_list 

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

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

33992  936 
val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes)); 
28054  937 
in 
938 
Code_Target.mk_serialization target 

34071  939 
(fn NONE => code_writeln  SOME file => File.write file o code_of_pretty) 
38779  940 
(rpair stmt_names' o code_of_pretty) p 
28054  941 
end; 
942 

943 
end; (*local*) 

944 

945 

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

946 
(** for instrumentalization **) 
28054  947 

34032  948 
fun evaluation_code_of thy target struct_name = 
38784  949 
Code_Target.serialize_custom thy (target, fn module_name => fn [] => 
950 
serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name); 

28054  951 

952 

953 
(** Isar setup **) 

954 

37821  955 
fun isar_serializer_sml module_name = 
33992  956 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
957 
>> (fn with_signatures => serialize_ml target_SML 

958 
print_sml_module print_sml_stmt module_name with_signatures)); 

28054  959 

37821  960 
fun isar_serializer_ocaml module_name = 
33992  961 
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true 
37748  962 
>> (fn with_signatures => serialize_ml target_OCaml 
33992  963 
print_ocaml_module print_ocaml_stmt module_name with_signatures)); 
28054  964 

965 
val setup = 

37821  966 
Code_Target.add_target 
37822
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

967 
(target_SML, { serializer = isar_serializer_sml, literals = literals_sml, 
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

968 
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

969 
make_command = fn isabelle => fn _ => isabelle ^ " r q u Pure" } }) 
37821  970 
#> Code_Target.add_target 
37822
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

971 
(target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml, 
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

972 
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

973 
make_command = fn ocaml => fn _ => ocaml ^ " w pu nums.cma ROOT.ocaml" } }) 
33992  974 
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36536
diff
changeset

975 
brackify_infix (1, R) fxy ( 
33992  976 
print_typ (INFX (1, X)) ty1, 
28054  977 
str ">", 
33992  978 
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

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

981 
brackify_infix (1, R) fxy ( 
33992  982 
print_typ (INFX (1, X)) ty1, 
28054  983 
str ">", 
33992  984 
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

985 
))) 
28054  986 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
987 
#> fold (Code_Target.add_reserved target_SML) 

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

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

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

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

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

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

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

997 
"virtual", "when", "while", "with" 

998 
] 

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

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

1001 
end; (*struct*) 