author  haftmann 
Mon, 07 Jun 2010 13:42:38 +0200  
changeset 37384  5aba26803073 
parent 37242  97097e589715 
child 37437  4202e11ae7dc 
permissions  rwrr 
36536  1 
(* Title: Tools/code/code_ml.ML 
28054  2 
Author: Florian Haftmann, TU Muenchen 
3 

4 
Serializer for SML and OCaml. 

5 
*) 

6 

7 
signature CODE_ML = 

8 
sig 

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

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

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

28054  14 
val setup: theory > theory 
15 
end; 

16 

17 
structure Code_ML : CODE_ML = 

18 
struct 

19 

20 
open Basic_Code_Thingol; 

21 
open Code_Printer; 

22 

23 
infixr 5 @@; 

24 
infixr 5 @; 

25 

33992  26 

27 
(** generic **) 

28 

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

31 

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

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

34 
 ML_Instance of string * ((class * (string * (vname * sort) list)) 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

35 
* (((class * (string * (string * dict list list))) list * (class * class) list list) 
28350  36 
* ((string * const) * (thm * bool)) list)); 
28054  37 

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

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

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

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

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

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

44 

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

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

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

47 

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

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

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

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

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

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

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

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

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

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

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

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

33992  62 

63 
(** SML serializer **) 

64 

65 
fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = 

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

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

70 
 print_tyco_expr fxy (tyco, tys) = 

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

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

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

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

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

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

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

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

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

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

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

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

85 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

87 
let 

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

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

90 
in case classrels 

91 
of [] => v_p 

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

93 
 classrels => brackets 

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

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

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

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

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

101 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

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

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

109 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

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

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

123 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

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

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

128 
then (str o deresolve) c 

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

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

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

137 
(print_term is_pseudo_fun) syntax_const some_thm vars 

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

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

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

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

152 
str "end" 
28054  153 
] 
154 
end 

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

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

28054  169 
) 
170 
end 

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

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

176 
let 

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

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

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

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

182 
str definer 

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

184 
:: str "=" 

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

186 
) 

187 
end; 

188 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

214 
in pair 

215 
(print_val_decl print_typscheme (name, vs_ty)) 

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

217 
print_eqn definer eq 

218 
:: map (print_eqn "") eqs 

219 
)) 

29189  220 
end 
33992  221 
 print_def is_pseudo_fun _ definer 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

235 
]; 
33992  236 
in pair 
237 
(print_val_decl print_dicttypscheme 

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

239 
(concat ( 

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

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

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

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

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

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

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

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

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

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

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

254 
((semicolon o map str) ( 

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

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

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

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

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

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

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

263 
 print_stmt (ML_Val binding) = 

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

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

267 
[sig_p] 

268 
(semicolon [p]) 

269 
end 

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

271 
let 

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

273 
fun print_pseudo_fun name = concat [ 

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

276 
str "=", 

277 
(str o deresolve) name, 

278 
str "();" 

279 
]; 

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

282 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

283 
in pair 

284 
sig_ps 

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

286 
end 

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

288 
let 

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

290 
in 

291 
pair 

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

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

294 
end 

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

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

299 
val (ps, p) = split_last sig_ps; 

300 
in pair 

301 
sig_ps 

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

303 
end 

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

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

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

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

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

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

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

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

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

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

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

320 
fun print_classparam_field (classparam, ty) = 

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

322 
fun print_classparam_proj (classparam, ty) = 

323 
print_proj (deresolve classparam) 

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

325 
in pair 

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

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

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

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

332 
(str o deresolve) class, 

333 
str "=", 

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

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

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

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

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

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

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

347 
else Pretty.chunks2 ( 

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

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

353 
:: body 

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

28054  355 
); 
356 

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

359 
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

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

361 
literal_positive_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_naive_numeral = string_of_int, 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

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

366 

28054  367 

368 
(** OCaml serializer **) 

369 

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

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

375 
 print_tyco_expr fxy (tyco, tys) = 

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

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

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

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

381 
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

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

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

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

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

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

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

390 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

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

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

394 
> fold_rev (fn classrel => fn p => 

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

396 
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); 

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

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

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

401 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 

31889  402 
str "_" 
35228  403 
 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

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

409 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

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

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

420 
 NONE => print_case is_pseudo_fun some_thm vars fxy cases) 

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

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

425 
then (str o deresolve) c 

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

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

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

434 
(print_term is_pseudo_fun) syntax_const some_thm vars 

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

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

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

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

28054  461 
) 
462 
end 

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

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

468 
let 

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

470 
 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

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

474 
str definer 

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

476 
:: str "=" 

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

478 
) 

479 
end; 

480 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

504 
concat ( 

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

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

514 
:: Pretty.brk 1 

515 
:: str "function" 

516 
:: Pretty.brk 1 

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

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

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

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

530 
Pretty.breaks dummy_parms 

531 
@ Pretty.brk 1 

532 
:: str "=" 

533 
:: Pretty.brk 1 

534 
:: str "match" 

535 
:: Pretty.brk 1 

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

537 
:: Pretty.brk 1 

538 
:: str "with" 

539 
:: Pretty.brk 1 

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

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

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

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

550 
(concat ( 

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

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

554 
)) 

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

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

556 
 print_def is_pseudo_fun _ definer 
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

570 
]; 
33992  571 
in pair 
572 
(print_val_decl print_dicttypscheme 

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

574 
(concat ( 

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

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

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

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

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

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

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

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

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

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

589 
((doublesemicolon o map str) ( 

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

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

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

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

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

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

597 
 print_stmt (ML_Val binding) = 

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

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

601 
[sig_p] 

602 
(doublesemicolon [p]) 

603 
end 

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

605 
let 

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

607 
fun print_pseudo_fun name = concat [ 

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

610 
str "=", 

611 
(str o deresolve) name, 

612 
str "();;" 

613 
]; 

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

616 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

617 
in pair 

618 
sig_ps 

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

620 
end 

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

622 
let 

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

624 
in 

625 
pair 

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

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

628 
end 

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

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

633 
val (ps, p) = split_last sig_ps; 

634 
in pair 

635 
sig_ps 

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

637 
end 

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

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

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

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

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

646 
fun print_classparam_field (classparam, ty) = 

647 
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

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

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

652 
val type_decl_p = concat [ 

653 
str ("type '" ^ v), 

654 
(str o deresolve) class, 

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

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

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

663 
(Pretty.chunks ( 

664 
doublesemicolon [type_decl_p] 

665 
:: map print_classparam_proj classparams 

666 
)) 

667 
end; 

668 
in print_stmt end; 

28054  669 

34032  670 
fun print_ocaml_module name some_decls body = if name = "" 
671 
then Pretty.chunks2 body 

672 
else 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; 

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

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, 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

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

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

708 

709 

28054  710 

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

712 

713 
local 

714 

715 
datatype ml_node = 

716 
Dummy of string 

717 
 Stmt of string * ml_stmt 

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

719 

720 
in 

721 

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

722 
fun ml_node_of_program labelled_name module_name reserved raw_module_alias program = 
28054  723 
let 
724 
val module_alias = if is_some module_name then K module_name else raw_module_alias; 

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

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

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

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

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

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

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

733 
let 

734 
val (x, nsp') = f nsp 

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

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

737 
let 

738 
val (x, nodes') = 

739 
nodes 

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

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

742 
let 

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

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

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

746 
fun map_nsp_fun_yield f (nsp_fun, nsp_typ) = 

747 
let 

748 
val (x, nsp_fun') = f nsp_fun 

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

750 
fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = 

751 
let 

752 
val (x, nsp_typ') = f nsp_typ 

753 
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

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

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

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

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

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

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

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

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

764 
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs 
35228  765 
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty 
766 
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

767 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

792 
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

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

794 
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

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

796 
end; 
28054  797 
fun add_datatypes stmts = 
798 
fold_map 

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

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

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

803 
 (name, _) => 

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

805 
) stmts 

806 
#>> (split_list #> apsnd (map_filter I 

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

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

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

809 
 stmts => ML_Datas stmts))); 
28054  810 
fun add_class stmts = 
811 
fold_map 

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

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

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

816 
 (name, Code_Thingol.Classparam _) => 

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

818 
 (name, _) => 

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

820 
) stmts 

821 
#>> (split_list #> apsnd (map_filter I 

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

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

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

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

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

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

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

830 
add_datatypes stmts 

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

832 
add_datatypes stmts 

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

834 
add_class stmts 

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

836 
add_class stmts 

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

838 
add_class stmts 

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

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

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

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

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

845 
fun add_stmts' stmts nsp_nodes = 

846 
let 

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

848 
val deps = 

849 
[] 

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

851 
> subtract (op =) names; 

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

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

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

856 
^ commas (map labelled_name names) 

857 
^ "\n" 

858 
^ commas module_names); 

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

859 
val module_name_path = Long_Name.explode module_name; 
28054  860 
fun add_dep name name' = 
861 
let 

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

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

865 
else let 

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

867 
(module_name_path, Long_Name.explode module_name'); 
28054  868 
in 
869 
map_node common 

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

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

872 
^ quote name ^ " > " ^ quote name' 

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

874 
end end; 

875 
in 

876 
nsp_nodes 

877 
> map_nsp_yield module_name_path (add_stmts stmts) 

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

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

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

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

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

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

884 
end; 

885 
val (_, nodes) = empty_module 

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

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

888 
fun deresolver prefix name = 

889 
let 

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

890 
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

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

894 
nodes 

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

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

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

898 
 Dummy stmt_name => stmt_name); 

899 
in 

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

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

903 
in (deresolver, nodes) end; 

904 

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

33992  909 
val presentation_stmt_names = Code_Target.stmt_names_of_destination destination; 
910 
val is_presentation = not (null presentation_stmt_names); 

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

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

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

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

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

922 
let 

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

924 
val p = if is_presentation then Pretty.chunks2 body 

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

926 
in SOME ([], p) end 

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

928 
o rev o flat o Graph.strong_conn) nodes 

929 
> split_list 

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

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

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

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

938 
(rpair stmt_names' o code_of_pretty) p destination 

28054  939 
end; 
940 

941 
end; (*local*) 

942 

943 

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

944 
(** for instrumentalization **) 
28054  945 

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

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

28054  949 

950 

951 
(** Isar setup **) 

952 

953 
fun isar_seri_sml module_name = 

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

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

959 
fun isar_seri_ocaml module_name = 

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

962 
print_ocaml_module print_ocaml_stmt module_name with_signatures)); 

28054  963 

964 
val setup = 

28064  965 
Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml)) 
966 
#> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml)) 

33992  967 
#> 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

968 
brackify_infix (1, R) fxy ( 
33992  969 
print_typ (INFX (1, X)) ty1, 
28054  970 
str ">", 
33992  971 
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

972 
))) 
33992  973 
#> 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

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

978 
))) 
28054  979 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
980 
#> fold (Code_Target.add_reserved target_SML) 

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

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

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

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

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

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

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

989 
"virtual", "when", "while", "with" 

990 
] 

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

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

993 
end; (*struct*) 