author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 50113  6c857312c9f5 
child 50625  e3d25e751d05 
permissions  rwrr 
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37449
diff
changeset

1 
(* Title: Tools/Code/code_ml.ML 
28054  2 
Author: Florian Haftmann, TU Muenchen 
3 

4 
Serializer for SML and OCaml. 

5 
*) 

6 

7 
signature CODE_ML = 

8 
sig 

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

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

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

13 

14 
structure Code_ML : CODE_ML = 

15 
struct 

16 

17 
open Basic_Code_Thingol; 

18 
open Code_Printer; 

19 

20 
infixr 5 @@; 

21 
infixr 5 @; 

22 

33992  23 

24 
(** generic **) 

25 

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

28 

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

29 
datatype ml_binding = 
35228  30 
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

31 
 ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list, 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

32 
superinsts: (class * (string * (string * dict list list))) list, 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

33 
inst_params: ((string * const) * (thm * bool)) list, 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

34 
superinst_params: ((string * const) * (thm * bool)) list }; 
28054  35 

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

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

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

39 
 ML_Funs of ml_binding list * string list 
48003
1d11af40b106
dropped sort constraints on datatype specifications
haftmann
parents:
47609
diff
changeset

40 
 ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list 
37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset

41 
 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

42 

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

45 
 print_product print xs = (SOME o enum " *" "" "") (map print xs); 
28054  46 

38922  47 
fun tuplify _ _ [] = NONE 
48 
 tuplify print fxy [x] = SOME (print fxy x) 

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

28054  50 

33992  51 

52 
(** SML serializer **) 

53 

47576  54 
fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve = 
28054  55 
let 
47609  56 
fun print_tyco_expr (tyco, []) = (str o deresolve) tyco 
57 
 print_tyco_expr (tyco, [ty]) = 

33992  58 
concat [print_typ BR ty, (str o deresolve) tyco] 
47609  59 
 print_tyco_expr (tyco, tys) = 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

60 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 
38923  61 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
47609  62 
of NONE => print_tyco_expr (tyco, tys) 
63 
 SOME (_, print) => print print_typ fxy tys) 

33992  64 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 
47609  65 
fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]); 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

66 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  67 
(map_filter (fn (v, sort) => 
68 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

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

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

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

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

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

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

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

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

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

78 
((str o deresolve) inst :: 
33992  79 
(if is_pseudo_fun inst then [str "()"] 
80 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

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

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

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

86 
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort)); 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

87 
fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

88 
print_app is_pseudo_fun some_thm vars fxy (const, []) 
35228  89 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 
31889  90 
str "_" 
35228  91 
 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

92 
str (lookup_var vars v) 
35228  93 
 print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = 
28054  94 
(case Code_Thingol.unfold_const_app t 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

95 
of SOME app => print_app is_pseudo_fun some_thm vars fxy app 
35228  96 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 
97 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

28054  99 
let 
31874  100 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
33992  101 
fun print_abs (pat, ty) = 
35228  102 
print_bind is_pseudo_fun some_thm NOBR pat 
28054  103 
#>> (fn p => concat [str "fn", p, str "=>"]); 
33992  104 
val (ps, vars') = fold_map print_abs binds vars; 
35228  105 
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

106 
 print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) = 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

107 
(case Code_Thingol.unfold_const_app (#primitive case_expr) 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

108 
of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c) 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

109 
then print_case is_pseudo_fun some_thm vars fxy case_expr 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

110 
else print_app is_pseudo_fun some_thm vars fxy app 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

111 
 NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

112 
and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) = 
29175  113 
if is_cons c then 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

114 
let val k = length dom in 
33992  115 
if k < 2 orelse length ts = k 
116 
then (str o deresolve) c 

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

120 
else if is_pseudo_fun c 
29175  121 
then (str o deresolve) c @@ str "()" 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

122 
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss 
35228  123 
@ map (print_term is_pseudo_fun some_thm vars BR) ts 
124 
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

38923  125 
(print_term is_pseudo_fun) const_syntax some_thm vars 
33992  126 
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

127 
and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } = 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

128 
(concat o map str) ["raise", "Fail", "\"empty case\""] 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

129 
 print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) = 
28054  130 
let 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

131 
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); 
47609  132 
fun print_match ((pat, _), t) vars = 
28054  133 
vars 
35228  134 
> print_bind is_pseudo_fun some_thm NOBR pat 
33992  135 
>> (fn p => semicolon [str "val", p, str "=", 
35228  136 
print_term is_pseudo_fun some_thm vars NOBR t]) 
33992  137 
val (ps, vars') = fold_map print_match binds vars; 
28054  138 
in 
139 
Pretty.chunks [ 

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

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

142 
str "end" 
28054  143 
] 
144 
end 

48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

145 
 print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = 
28054  146 
let 
33992  147 
fun print_select delim (pat, body) = 
28054  148 
let 
35228  149 
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; 
28054  150 
in 
35228  151 
concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body] 
28054  152 
end; 
153 
in 

31665  154 
brackets ( 
28054  155 
str "case" 
35228  156 
:: print_term is_pseudo_fun some_thm vars NOBR t 
33992  157 
:: print_select "of" clause 
158 
:: map (print_select "") clauses 

28054  159 
) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

160 
end; 
33992  161 
fun print_val_decl print_typscheme (name, typscheme) = concat 
162 
[str "val", str (deresolve name), str ":", print_typscheme typscheme]; 

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

164 
let 

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

167 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  168 
in 
169 
concat ( 

170 
str definer 

48003
1d11af40b106
dropped sort constraints on datatype specifications
haftmann
parents:
47609
diff
changeset

171 
:: print_tyco_expr (tyco, map ITyVar vs) 
33992  172 
:: str "=" 
173 
:: separate (str "") (map print_co cos) 

174 
) 

175 
end; 

176 
fun print_def is_pseudo_fun needs_typ definer 

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

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

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

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

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

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

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

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

187 
val prolog = if needs_typ then 
33992  188 
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

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

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

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

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

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

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

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

199 
end 
33992  200 
val shift = if null eqs then I else 
201 
map (Pretty.block o single o Pretty.block o single); 

202 
in pair 

203 
(print_val_decl print_typscheme (name, vs_ty)) 

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

205 
print_eqn definer eq 

206 
:: map (print_eqn "") eqs 

207 
)) 

29189  208 
end 
33992  209 
 print_def is_pseudo_fun _ definer 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

210 
(ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) = 
29189  211 
let 
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40627
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

223 
]; 
33992  224 
in pair 
225 
(print_val_decl print_dicttypscheme 

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

227 
(concat ( 

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

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

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

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

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

233 
:: enum "," "{" "}" 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

234 
(map print_super_instance superinsts 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

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

236 
:: str ":" 
47609  237 
@@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs]) 
33992  238 
)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

239 
end; 
33992  240 
fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair 
241 
[print_val_decl print_typscheme (name, vs_ty)] 

242 
((semicolon o map str) ( 

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

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

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

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

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

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

248 
:: "Fail" 
33992  249 
@@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name 
250 
)) 

251 
 print_stmt (ML_Val binding) = 

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

252 
let 
33992  253 
val (sig_p, p) = print_def (K false) true "val" binding 
254 
in pair 

255 
[sig_p] 

256 
(semicolon [p]) 

257 
end 

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

259 
let 

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

261 
fun print_pseudo_fun name = concat [ 

29189  262 
str "val", 
263 
(str o deresolve) name, 

264 
str "=", 

265 
(str o deresolve) name, 

266 
str "();" 

267 
]; 

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

270 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

271 
in pair 

272 
sig_ps 

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

274 
end 

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

276 
let 

48003
1d11af40b106
dropped sort constraints on datatype specifications
haftmann
parents:
47609
diff
changeset

277 
val ty_p = print_tyco_expr (tyco, map ITyVar vs); 
33992  278 
in 
279 
pair 

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

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

282 
end 

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

28054  284 
let 
33992  285 
val sig_ps = print_datatype_decl "datatype" data 
286 
:: map (print_datatype_decl "and") datas; 

287 
val (ps, p) = split_last sig_ps; 

288 
in pair 

289 
sig_ps 

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

291 
end 

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

292 
 print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = 
28054  293 
let 
33992  294 
fun print_field s p = concat [str s, str ":", p]; 
295 
fun print_proj s p = semicolon 

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

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

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

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

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

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

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

304 
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v))); 
33992  305 
fun print_classparam_decl (classparam, ty) = 
306 
print_val_decl print_typscheme 

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

308 
fun print_classparam_field (classparam, ty) = 

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

310 
fun print_classparam_proj (classparam, ty) = 

311 
print_proj (deresolve classparam) 

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

313 
in pair 

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

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

315 
:: map print_super_class_decl super_classes 
33992  316 
@ map print_classparam_decl classparams) 
317 
(Pretty.chunks ( 

28054  318 
concat [ 
319 
str ("type '" ^ v), 

320 
(str o deresolve) class, 

321 
str "=", 

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

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

323 
map print_super_class_field super_classes 
33992  324 
@ map print_classparam_field classparams 
28054  325 
) 
326 
] 

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

327 
:: map print_super_class_proj super_classes 
33992  328 
@ map print_classparam_proj classparams 
329 
)) 

28054  330 
end; 
33992  331 
in print_stmt end; 
28054  332 

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

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

334 
Pretty.chunks2 ( 
33992  335 
Pretty.chunks ( 
336 
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

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

340 
:: body 

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

28054  342 
); 
343 

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

346 
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

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

348 
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

349 
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

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

351 
literal_list = enum "," "[" "]", 
28064  352 
infix_cons = (7, "::") 
353 
}; 

354 

28054  355 

356 
(** OCaml serializer **) 

357 

47576  358 
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve = 
28054  359 
let 
47609  360 
fun print_tyco_expr (tyco, []) = (str o deresolve) tyco 
361 
 print_tyco_expr (tyco, [ty]) = 

33992  362 
concat [print_typ BR ty, (str o deresolve) tyco] 
47609  363 
 print_tyco_expr (tyco, tys) = 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

364 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] 
38923  365 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
47609  366 
of NONE => print_tyco_expr (tyco, tys) 
47576  367 
 SOME (_, print) => print print_typ fxy tys) 
33992  368 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 
47609  369 
fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]); 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

370 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  371 
(map_filter (fn (v, sort) => 
372 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

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

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

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

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

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

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

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

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

381 
brackify BR ((str o deresolve) inst :: 
33992  382 
(if is_pseudo_fun inst then [str "()"] 
383 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 

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

384 
 print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = 
33992  385 
str (if k = 1 then "_" ^ first_upper v 
386 
else "_" ^ first_upper v ^ string_of_int (i+1)) 

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

389 
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort)); 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

390 
fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

391 
print_app is_pseudo_fun some_thm vars fxy (const, []) 
35228  392 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 
31889  393 
str "_" 
35228  394 
 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

395 
str (lookup_var vars v) 
35228  396 
 print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = 
28054  397 
(case Code_Thingol.unfold_const_app t 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

398 
of SOME app => print_app is_pseudo_fun some_thm vars fxy app 
35228  399 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 
400 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

406 
 print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) = 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

407 
(case Code_Thingol.unfold_const_app (#primitive case_expr) 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

408 
of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c) 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

409 
then print_case is_pseudo_fun some_thm vars fxy case_expr 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

410 
else print_app is_pseudo_fun some_thm vars fxy app 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

411 
 NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

412 
and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) = 
28054  413 
if is_cons c then 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

414 
let val k = length dom in 
33992  415 
if length ts = k 
416 
then (str o deresolve) c 

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

420 
else if is_pseudo_fun c 
29175  421 
then (str o deresolve) c @@ str "()" 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

422 
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss 
35228  423 
@ map (print_term is_pseudo_fun some_thm vars BR) ts 
424 
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

38923  425 
(print_term is_pseudo_fun) const_syntax some_thm vars 
33992  426 
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

427 
and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } = 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

428 
(concat o map str) ["failwith", "\"empty case\""] 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

429 
 print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) = 
28054  430 
let 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

431 
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); 
47576  432 
fun print_let ((pat, _), t) vars = 
28054  433 
vars 
35228  434 
> print_bind is_pseudo_fun some_thm NOBR pat 
28054  435 
>> (fn p => concat 
35228  436 
[str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) 
33992  437 
val (ps, vars') = fold_map print_let binds vars; 
31665  438 
in 
439 
brackify_block fxy (Pretty.chunks ps) [] 

35228  440 
(print_term is_pseudo_fun some_thm vars' NOBR body) 
31665  441 
end 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

442 
 print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = 
28054  443 
let 
33992  444 
fun print_select delim (pat, body) = 
28054  445 
let 
35228  446 
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; 
447 
in concat [str delim, p, str ">", print_term is_pseudo_fun some_thm vars' NOBR body] end; 

28054  448 
in 
31665  449 
brackets ( 
28054  450 
str "match" 
35228  451 
:: print_term is_pseudo_fun some_thm vars NOBR t 
33992  452 
:: print_select "with" clause 
453 
:: map (print_select "") clauses 

28054  454 
) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

455 
end; 
33992  456 
fun print_val_decl print_typscheme (name, typscheme) = concat 
457 
[str "val", str (deresolve name), str ":", print_typscheme typscheme]; 

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

459 
let 

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

462 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  463 
in 
464 
concat ( 

465 
str definer 

48003
1d11af40b106
dropped sort constraints on datatype specifications
haftmann
parents:
47609
diff
changeset

466 
:: print_tyco_expr (tyco, map ITyVar vs) 
33992  467 
:: str "=" 
468 
:: separate (str "") (map print_co cos) 

469 
) 

470 
end; 

471 
fun print_def is_pseudo_fun needs_typ definer 

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

28054  473 
let 
35228  474 
fun print_eqn ((ts, t), (some_thm, _)) = 
28054  475 
let 
32913  476 
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

477 
val vars = reserved 
42599
1a82b0400b2a
improving naming of fresh variables in OCaml serializer
bulwahn
parents:
41952
diff
changeset

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

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

480 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  481 
(insert (op =)) ts []); 
482 
in concat [ 

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

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

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

494 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  495 
(insert (op =)) ts []); 
496 
in 

497 
concat ( 

29189  498 
(if is_pseudo then [str "()"] 
35228  499 
else map (print_term is_pseudo_fun some_thm vars BR) ts) 
28054  500 
@ str "=" 
35228  501 
@@ print_term is_pseudo_fun some_thm vars NOBR t 
28054  502 
) 
503 
end 

33992  504 
 print_eqns _ ((eq as (([_], _), _)) :: eqs) = 
28054  505 
Pretty.block ( 
506 
str "=" 

507 
:: Pretty.brk 1 

508 
:: str "function" 

509 
:: Pretty.brk 1 

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

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

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

520 
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs; 
28054  521 
in 
522 
Pretty.block ( 

523 
Pretty.breaks dummy_parms 

524 
@ Pretty.brk 1 

525 
:: str "=" 

526 
:: Pretty.brk 1 

527 
:: str "match" 

528 
:: Pretty.brk 1 

38778  529 
:: (Pretty.block o commas) dummy_parms 
28054  530 
:: Pretty.brk 1 
531 
:: str "with" 

532 
:: Pretty.brk 1 

33992  533 
:: print_eqn eq 
28054  534 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  535 
o single o print_eqn) eqs' 
28054  536 
) 
537 
end; 

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

538 
val prolog = if needs_typ then 
33992  539 
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

540 
else (concat o map str) [definer, deresolve name]; 
33992  541 
in pair 
542 
(print_val_decl print_typscheme (name, vs_ty)) 

543 
(concat ( 

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

544 
prolog 
33992  545 
:: print_dict_args vs 
546 
@ print_eqns (is_pseudo_fun name) eqs 

547 
)) 

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

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

549 
 print_def is_pseudo_fun _ definer 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

550 
(ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

563 
]; 
33992  564 
in pair 
565 
(print_val_decl print_dicttypscheme 

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

567 
(concat ( 

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

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

569 
:: (str o deresolve) inst 
43343
e83695ea0e0a
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
bulwahn
parents:
42599
diff
changeset

570 
:: (if is_pseudo_fun inst then [str "()"] 
e83695ea0e0a
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
bulwahn
parents:
42599
diff
changeset

571 
else print_dict_args vs) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

573 
@@ brackets [ 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

574 
enum_default "()" ";" "{" "}" (map print_super_instance superinsts 
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

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

576 
str ":", 
47609  577 
print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs]) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

580 
end; 
33992  581 
fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair 
582 
[print_val_decl print_typscheme (name, vs_ty)] 

583 
((doublesemicolon o map str) ( 

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

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

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

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

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

588 
:: "failwith" 
33992  589 
@@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name 
590 
)) 

591 
 print_stmt (ML_Val binding) = 

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

592 
let 
33992  593 
val (sig_p, p) = print_def (K false) true "let" binding 
594 
in pair 

595 
[sig_p] 

596 
(doublesemicolon [p]) 

597 
end 

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

599 
let 

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

601 
fun print_pseudo_fun name = concat [ 

29189  602 
str "let", 
603 
(str o deresolve) name, 

604 
str "=", 

605 
(str o deresolve) name, 

606 
str "();;" 

607 
]; 

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

610 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 

611 
in pair 

612 
sig_ps 

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

614 
end 

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

616 
let 

48003
1d11af40b106
dropped sort constraints on datatype specifications
haftmann
parents:
47609
diff
changeset

617 
val ty_p = print_tyco_expr (tyco, map ITyVar vs); 
33992  618 
in 
619 
pair 

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

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

622 
end 

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

28054  624 
let 
33992  625 
val sig_ps = print_datatype_decl "type" data 
626 
:: map (print_datatype_decl "and") datas; 

627 
val (ps, p) = split_last sig_ps; 

628 
in pair 

629 
sig_ps 

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

631 
end 

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

632 
 print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = 
28054  633 
let 
33992  634 
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

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

636 
print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v)); 
33992  637 
fun print_classparam_decl (classparam, ty) = 
638 
print_val_decl print_typscheme 

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

640 
fun print_classparam_field (classparam, ty) = 

641 
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

642 
val w = "_" ^ first_upper v; 
33992  643 
fun print_classparam_proj (classparam, _) = 
644 
(concat o map str) ["let", deresolve classparam, w, "=", 

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

646 
val type_decl_p = concat [ 

647 
str ("type '" ^ v), 

648 
(str o deresolve) class, 

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

651 
map print_super_class_field super_classes 
33992  652 
@ map print_classparam_field classparams 
653 
) 

28054  654 
]; 
33992  655 
in pair 
656 
(type_decl_p :: map print_classparam_decl classparams) 

657 
(Pretty.chunks ( 

658 
doublesemicolon [type_decl_p] 

659 
:: map print_classparam_proj classparams 

660 
)) 

661 
end; 

662 
in print_stmt end; 

28054  663 

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

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

665 
Pretty.chunks2 ( 
33992  666 
Pretty.chunks ( 
667 
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

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

671 
:: body 

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

28054  673 
); 
674 

28064  675 
val literals_ocaml = let 
676 
fun chr i = 

677 
let 

678 
val xs = string_of_int i; 

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

679 
val ys = replicate_string (3  length (raw_explode xs)) "0"; 
28064  680 
in "\\" ^ ys ^ xs end; 
681 
fun char_ocaml c = 

682 
let 

683 
val i = ord c; 

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

685 
then chr i else c 

686 
in s end; 

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

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

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

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

690 
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

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

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

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

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

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

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

699 
literal_list = enum ";" "[" "]", 
28064  700 
infix_cons = (6, "::") 
701 
} end; 

702 

703 

28054  704 

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

706 

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

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

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

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

710 
let 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42599
diff
changeset

711 
val (base', nsp_const') = 
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42599
diff
changeset

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

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

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

715 
let 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42599
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

734 
in (ML_Function (name, (tysm, eqs')), some_value_name) end 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

753 
fun modify_datatypes stmts = single (SOME 

754 
(ML_Datas (map_filter 

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

756 
fun modify_class stmts = single (SOME 

757 
(ML_Class (the_single (map_filter 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

784 

47576  785 
fun serialize_ml print_ml_module print_ml_stmt with_signatures 
39142  786 
{ labelled_name, reserved_syms, includes, module_alias, 
41343  787 
class_syntax, tyco_syntax, const_syntax } program = 
28054  788 
let 
39147  789 

790 
(* build program *) 

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

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

792 
ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program; 
39147  793 

794 
(* print statements *) 

795 
fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt 

47576  796 
tyco_syntax const_syntax (make_vars reserved_syms) 
39147  797 
(Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt 
798 
> apfst SOME; 

799 

800 
(* print modules *) 

47576  801 
fun print_module _ base _ xs = 
39147  802 
let 
803 
val (raw_decls, body) = split_list xs; 

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

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

806 

807 
(* serialization *) 

808 
val p = Pretty.chunks2 (map snd includes 

809 
@ map snd (Code_Namespace.print_hierarchical { 

810 
print_module = print_module, print_stmt = print_stmt, 

811 
lift_markup = apsnd } ml_program)); 

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

48568  814 
fun prepare names width p = ([("", format names width p)], try (deresolver [])); 
28054  815 
in 
48568  816 
Code_Target.serialization write prepare p 
28054  817 
end; 
818 

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

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

38966  827 

828 
(** Isar setup **) 

829 

28054  830 
val setup = 
37821  831 
Code_Target.add_target 
38966  832 
(target_SML, { serializer = serializer_sml, literals = literals_sml, 
41940  833 
check = { env_var = "ISABELLE_PROCESS", 
834 
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), 

50022
286dfcab9833
restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
haftmann
parents:
48568
diff
changeset

835 
make_command = fn _ => 
50113  836 
"\"$ISABELLE_PROCESS\" r q e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' Pure" } }) 
37821  837 
#> Code_Target.add_target 
38966  838 
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, 
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP  discontinued implicit detection;
wenzelm
parents:
41940
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

865 
"virtual", "when", "while", "with" 

866 
] 

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

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

869 
end; (*struct*) 