author  haftmann 
Fri, 24 Apr 2020 13:16:40 +0000  
changeset 71798  fc4f9dad5292 
parent 70352  ce3c1d8791eb 
child 71803  14914ae80f70 
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 
end; 
12 

13 
structure Code_ML : CODE_ML = 

14 
struct 

15 

55150  16 
open Basic_Code_Symbol; 
28054  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) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

31 
 ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list, 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

32 
superinsts: (class * dict list list) list, 
52519
598addf65209
explicit hint for domain of class parameters in instance statements
haftmann
parents:
52435
diff
changeset

33 
inst_params: ((string * (const * int)) * (thm * bool)) list, 
598addf65209
explicit hint for domain of class parameters in instance statements
haftmann
parents:
52435
diff
changeset

34 
superinst_params: ((string * (const * int)) * (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 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

39 
 ML_Funs of (Code_Namespace.export * ml_binding) list * Code_Symbol.T 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 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

41 
 ML_Class of string * (vname * ((class * class) 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 

68028  54 
fun print_sml_char c = 
55 
if c = "\\" 

56 
then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*) 

57 
else if Symbol.is_ascii c 

69207  58 
then ML_Syntax.print_symbol_char c 
68028  59 
else error "nonASCII byte in SML string literal"; 
59456
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

60 

68028  61 
val print_sml_string = quote o translate_string print_sml_char; 
59456
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

62 

50625  63 
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve = 
28054  64 
let 
55150  65 
val deresolve_const = deresolve o Constant; 
66 
val deresolve_classrel = deresolve o Class_Relation; 

67 
val deresolve_inst = deresolve o Class_Instance; 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

68 
fun print_tyco_expr (sym, []) = (str o deresolve) sym 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

69 
 print_tyco_expr (sym, [ty]) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

70 
concat [print_typ BR ty, (str o deresolve) sym] 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

71 
 print_tyco_expr (sym, tys) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

72 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] 
38923  73 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
55150  74 
of NONE => print_tyco_expr (Type_Constructor tyco, tys) 
47609  75 
 SOME (_, print) => print print_typ fxy tys) 
33992  76 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 
55150  77 
fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]); 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

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

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

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

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

83 
fun print_classrels fxy [] ps = brackify fxy ps 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

85 
 print_classrels fxy classrels ps = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

89 
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

90 
((str o deresolve_inst) inst :: 
55150  91 
(if is_pseudo_fun (Class_Instance inst) then [str "()"] 
33992  92 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 
63303  93 
 print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = 
62539  94 
[str (if length = 1 then Name.enforce_case true var ^ "_" 
95 
else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")] 

38922  96 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  97 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 
63303  98 
(map_index (fn (i, _) => Dict ([], 
99 
Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort)); 

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

100 
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

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

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

108 
of SOME app => print_app is_pseudo_fun some_thm vars fxy app 
35228  109 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 
110 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

119 
 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

120 
(case Code_Thingol.unfold_const_app (#primitive case_expr) 
55150  121 
of SOME (app as ({ sym = Constant const, ... }, _)) => 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

122 
if is_none (const_syntax const) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

123 
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

124 
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

125 
 NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

126 
and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

127 
if is_constr sym then 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

128 
let val k = length dom in 
33992  129 
if k < 2 orelse length ts = k 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

130 
then (str o deresolve) sym 
38922  131 
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) 
35228  132 
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] 
33992  133 
end 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

134 
else if is_pseudo_fun sym 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

135 
then (str o deresolve) sym @@ str "()" 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

136 
else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss 
35228  137 
@ map (print_term is_pseudo_fun some_thm vars BR) ts 
138 
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

38923  139 
(print_term is_pseudo_fun) const_syntax some_thm vars 
33992  140 
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

141 
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

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

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

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

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

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

156 
str "end" 
28054  157 
] 
158 
end 

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

159 
 print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = 
28054  160 
let 
33992  161 
fun print_select delim (pat, body) = 
28054  162 
let 
35228  163 
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; 
28054  164 
in 
35228  165 
concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body] 
28054  166 
end; 
167 
in 

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

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

174 
end; 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

175 
fun print_val_decl print_typscheme (sym, typscheme) = concat 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

176 
[str "val", str (deresolve sym), str ":", print_typscheme typscheme]; 
33992  177 
fun print_datatype_decl definer (tyco, (vs, cos)) = 
178 
let 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

179 
fun print_co ((co, _), []) = str (deresolve_const co) 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

180 
 print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

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

184 
str definer 

55150  185 
:: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) 
33992  186 
:: str "=" 
187 
:: separate (str "") (map print_co cos) 

188 
) 

189 
end; 

190 
fun print_def is_pseudo_fun needs_typ definer 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

191 
(ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) = 
29189  192 
let 
35228  193 
fun print_eqn definer ((ts, t), (some_thm, _)) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

195 
val vars = reserved 
55145
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

196 
> intro_base_names_for (is_none o const_syntax) 
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

197 
deresolve (t :: ts) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

200 
val prolog = if needs_typ then 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

201 
concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

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

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

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

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

215 
in pair 

55150  216 
(print_val_decl print_typscheme (Constant const, vs_ty)) 
33992  217 
((Pretty.block o Pretty.fbreaks o shift) ( 
218 
print_eqn definer eq 

219 
:: map (print_eqn "") eqs 

220 
)) 

29189  221 
end 
33992  222 
 print_def is_pseudo_fun _ definer 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

223 
(ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) = 
29189  224 
let 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

226 
concat [ 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

227 
(str o Long_Name.base_name o deresolve_classrel) (class, super_class), 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

228 
str "=", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

230 
]; 
52519
598addf65209
explicit hint for domain of class parameters in instance statements
haftmann
parents:
52435
diff
changeset

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

232 
concat [ 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

236 
]; 
33992  237 
in pair 
238 
(print_val_decl print_dicttypscheme 

55150  239 
(Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) 
33992  240 
(concat ( 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

241 
str definer 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

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

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

249 
:: str ":" 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

250 
@@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) 
33992  251 
)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

252 
end; 
55681  253 
fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair 
55150  254 
[print_val_decl print_typscheme (Constant const, vs_ty)] 
33992  255 
((semicolon o map str) ( 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

256 
(if n = 0 then "val" else "fun") 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

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

261 
:: "Fail" 
68028  262 
@@ print_sml_string const 
33992  263 
)) 
55681  264 
 print_stmt _ (ML_Val binding) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

268 
[sig_p] 

269 
(semicolon [p]) 

270 
end 

55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

271 
 print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) = 
33992  272 
let 
273 
val print_def' = print_def (member (op =) pseudo_funs) false; 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

274 
fun print_pseudo_fun sym = concat [ 
29189  275 
str "val", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

276 
(str o deresolve) sym, 
29189  277 
str "=", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

278 
(str o deresolve) sym, 
29189  279 
str "();" 
280 
]; 

33992  281 
val (sig_ps, (ps, p)) = (apsnd split_last o split_list) 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

282 
(print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings); 
33992  283 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 
284 
in pair 

55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

285 
(map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE) 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

286 
((export :: map fst exports_bindings) ~~ sig_ps)) 
33992  287 
(Pretty.chunks (ps @ semicolon [p] :: pseudo_ps)) 
288 
end 

55681  289 
 print_stmt _ (ML_Datas [(tyco, (vs, []))]) = 
33992  290 
let 
55150  291 
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); 
33992  292 
in 
293 
pair 

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

55681  295 
(semicolon [str "datatype", ty_p, str "=", str "EMPTY__"]) 
33992  296 
end 
55681  297 
 print_stmt export (ML_Datas (data :: datas)) = 
28054  298 
let 
55681  299 
val decl_ps = print_datatype_decl "datatype" data 
33992  300 
:: map (print_datatype_decl "and") datas; 
55681  301 
val (ps, p) = split_last decl_ps; 
33992  302 
in pair 
55681  303 
(if Code_Namespace.is_public export 
304 
then decl_ps 

305 
else map (fn (tyco, (vs, _)) => 

306 
concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) 

307 
(data :: datas)) 

33992  308 
(Pretty.chunks (ps @ semicolon [p])) 
309 
end 

55681  310 
 print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = 
28054  311 
let 
33992  312 
fun print_field s p = concat [str s, str ":", p]; 
313 
fun print_proj s p = semicolon 

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

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

315 
fun print_super_class_decl (classrel as (_, super_class)) = 
33992  316 
print_val_decl print_dicttypscheme 
55150  317 
(Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v))); 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

318 
fun print_super_class_field (classrel as (_, super_class)) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

319 
print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

320 
fun print_super_class_proj (classrel as (_, super_class)) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

321 
print_proj (deresolve_classrel classrel) 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

322 
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v))); 
33992  323 
fun print_classparam_decl (classparam, ty) = 
324 
print_val_decl print_typscheme 

55150  325 
(Constant classparam, ([(v, [class])], ty)); 
33992  326 
fun print_classparam_field (classparam, ty) = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

327 
print_field (deresolve_const classparam) (print_typ NOBR ty); 
33992  328 
fun print_classparam_proj (classparam, ty) = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

329 
print_proj (deresolve_const classparam) 
33992  330 
(print_typscheme ([(v, [class])], ty)); 
331 
in pair 

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

55681  333 
:: (if Code_Namespace.is_public export 
334 
then map print_super_class_decl classrels 

335 
@ map print_classparam_decl classparams 

336 
else [])) 

33992  337 
(Pretty.chunks ( 
28054  338 
concat [ 
55681  339 
str "type", 
340 
print_dicttyp (class, ITyVar v), 

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

342 
enum "," "{" "};" ( 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

343 
map print_super_class_field classrels 
33992  344 
@ map print_classparam_field classparams 
28054  345 
) 
346 
] 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

347 
:: map print_super_class_proj classrels 
33992  348 
@ map print_classparam_proj classparams 
349 
)) 

28054  350 
end; 
33992  351 
in print_stmt end; 
28054  352 

55677  353 
fun print_sml_module name decls body = 
38933
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38928
diff
changeset

354 
Pretty.chunks2 ( 
55677  355 
Pretty.chunks [ 
356 
str ("structure " ^ name ^ " : sig"), 

357 
(indent 2 o Pretty.chunks) decls, 

358 
str "end = struct" 

359 
] 

33992  360 
:: body 
361 
@ str ("end; (*struct " ^ name ^ "*)") 

28054  362 
); 
363 

28064  364 
val literals_sml = Literals { 
68028  365 
literal_string = print_sml_string, 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

366 
literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)", 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

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

370 

28054  371 

372 
(** OCaml serializer **) 

373 

68028  374 
val print_ocaml_string = 
375 
let 

376 
fun chr i = 

377 
let 

378 
val xs = string_of_int i; 

379 
val ys = replicate_string (3  length (raw_explode xs)) "0"; 

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

381 
fun char c = 

382 
let 

383 
val i = ord c; 

384 
val s = 

385 
if i >= 128 then error "nonASCII byte in OCaml string literal" 

386 
else if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126 

387 
then chr i else c 

388 
in s end; 

389 
in quote o translate_string char end; 

390 

50625  391 
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve = 
28054  392 
let 
55150  393 
val deresolve_const = deresolve o Constant; 
394 
val deresolve_classrel = deresolve o Class_Relation; 

395 
val deresolve_inst = deresolve o Class_Instance; 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

396 
fun print_tyco_expr (sym, []) = (str o deresolve) sym 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

397 
 print_tyco_expr (sym, [ty]) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

398 
concat [print_typ BR ty, (str o deresolve) sym] 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

399 
 print_tyco_expr (sym, tys) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

400 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] 
38923  401 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
55150  402 
of NONE => print_tyco_expr (Type_Constructor tyco, tys) 
47576  403 
 SOME (_, print) => print print_typ fxy tys) 
33992  404 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 
55150  405 
fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]); 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

406 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  407 
(map_filter (fn (v, sort) => 
408 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

410 
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

411 
val print_classrels = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

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

416 
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

417 
brackify BR ((str o deresolve_inst) inst :: 
55150  418 
(if is_pseudo_fun (Class_Instance inst) then [str "()"] 
33992  419 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 
63303  420 
 print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = 
62539  421 
str (if length = 1 then "_" ^ Name.enforce_case true var 
422 
else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1)) 

38922  423 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  424 
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR 
63303  425 
(map_index (fn (i, _) => Dict ([], 
426 
Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort)); 

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

427 
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

428 
print_app is_pseudo_fun some_thm vars fxy (const, []) 
35228  429 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 
31889  430 
str "_" 
35228  431 
 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

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

435 
of SOME app => print_app is_pseudo_fun some_thm vars fxy app 
35228  436 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 
437 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

28054  439 
let 
31874  440 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
35228  441 
val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars; 
442 
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

443 
 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

444 
(case Code_Thingol.unfold_const_app (#primitive case_expr) 
55150  445 
of SOME (app as ({ sym = Constant const, ... }, _)) => 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

446 
if is_none (const_syntax const) 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

447 
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

448 
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

449 
 NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

450 
and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

451 
if is_constr sym then 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

452 
let val k = length dom in 
33992  453 
if length ts = k 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

454 
then (str o deresolve) sym 
38922  455 
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) 
35228  456 
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] 
33992  457 
end 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

458 
else if is_pseudo_fun sym 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

459 
then (str o deresolve) sym @@ str "()" 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

460 
else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss 
35228  461 
@ map (print_term is_pseudo_fun some_thm vars BR) ts 
462 
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) 

38923  463 
(print_term is_pseudo_fun) const_syntax some_thm vars 
33992  464 
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

465 
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

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

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

469 
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); 
47576  470 
fun print_let ((pat, _), t) vars = 
28054  471 
vars 
35228  472 
> print_bind is_pseudo_fun some_thm NOBR pat 
28054  473 
>> (fn p => concat 
35228  474 
[str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) 
33992  475 
val (ps, vars') = fold_map print_let binds vars; 
31665  476 
in 
61129
774752af4a1f
parenthesing letexpressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59456
diff
changeset

477 
brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body] 
31665  478 
end 
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
48003
diff
changeset

479 
 print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = 
28054  480 
let 
33992  481 
fun print_select delim (pat, body) = 
28054  482 
let 
35228  483 
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; 
484 
in concat [str delim, p, str ">", print_term is_pseudo_fun some_thm vars' NOBR body] end; 

28054  485 
in 
31665  486 
brackets ( 
28054  487 
str "match" 
35228  488 
:: print_term is_pseudo_fun some_thm vars NOBR t 
33992  489 
:: print_select "with" clause 
490 
:: map (print_select "") clauses 

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

492 
end; 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

493 
fun print_val_decl print_typscheme (sym, typscheme) = concat 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

494 
[str "val", str (deresolve sym), str ":", print_typscheme typscheme]; 
33992  495 
fun print_datatype_decl definer (tyco, (vs, cos)) = 
496 
let 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

497 
fun print_co ((co, _), []) = str (deresolve_const co) 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

498 
 print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34071
diff
changeset

499 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  500 
in 
501 
concat ( 

502 
str definer 

55150  503 
:: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) 
33992  504 
:: str "=" 
505 
:: separate (str "") (map print_co cos) 

506 
) 

507 
end; 

508 
fun print_def is_pseudo_fun needs_typ definer 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

509 
(ML_Function (const, (vs_ty as (vs, ty), eqs))) = 
28054  510 
let 
35228  511 
fun print_eqn ((ts, t), (some_thm, _)) = 
28054  512 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

513 
val vars = reserved 
55145
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

514 
> intro_base_names_for (is_none o const_syntax) 
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

515 
deresolve (t :: ts) 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

516 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  517 
(insert (op =)) ts []); 
518 
in concat [ 

38778  519 
(Pretty.block o commas) 
35228  520 
(map (print_term is_pseudo_fun some_thm vars NOBR) ts), 
28054  521 
str ">", 
35228  522 
print_term is_pseudo_fun some_thm vars NOBR t 
28054  523 
] end; 
35228  524 
fun print_eqns is_pseudo [((ts, t), (some_thm, _))] = 
28054  525 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

526 
val vars = reserved 
55145
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

527 
> intro_base_names_for (is_none o const_syntax) 
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

528 
deresolve (t :: ts) 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

529 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  530 
(insert (op =)) ts []); 
531 
in 

532 
concat ( 

29189  533 
(if is_pseudo then [str "()"] 
35228  534 
else map (print_term is_pseudo_fun some_thm vars BR) ts) 
28054  535 
@ str "=" 
35228  536 
@@ print_term is_pseudo_fun some_thm vars NOBR t 
28054  537 
) 
538 
end 

33992  539 
 print_eqns _ ((eq as (([_], _), _)) :: eqs) = 
28054  540 
Pretty.block ( 
541 
str "=" 

542 
:: Pretty.brk 1 

543 
:: str "function" 

544 
:: Pretty.brk 1 

33992  545 
:: print_eqn eq 
28054  546 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  547 
o single o print_eqn) eqs 
28054  548 
) 
33992  549 
 print_eqns _ (eqs as eq :: eqs') = 
28054  550 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

551 
val vars = reserved 
55145
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

552 
> intro_base_names_for (is_none o const_syntax) 
2bb3cd36bcf7
more abstract declaration of unqualified constant names in code printing context
haftmann
parents:
52519
diff
changeset

553 
deresolve (map (snd o fst) eqs) 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

554 
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs; 
28054  555 
in 
556 
Pretty.block ( 

557 
Pretty.breaks dummy_parms 

558 
@ Pretty.brk 1 

559 
:: str "=" 

560 
:: Pretty.brk 1 

561 
:: str "match" 

562 
:: Pretty.brk 1 

38778  563 
:: (Pretty.block o commas) dummy_parms 
28054  564 
:: Pretty.brk 1 
565 
:: str "with" 

566 
:: Pretty.brk 1 

33992  567 
:: print_eqn eq 
28054  568 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  569 
o single o print_eqn) eqs' 
28054  570 
) 
571 
end; 

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

572 
val prolog = if needs_typ then 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

573 
concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

574 
else (concat o map str) [definer, deresolve_const const]; 
33992  575 
in pair 
55150  576 
(print_val_decl print_typscheme (Constant const, vs_ty)) 
33992  577 
(concat ( 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

578 
prolog 
33992  579 
:: print_dict_args vs 
55150  580 
@ print_eqns (is_pseudo_fun (Constant const)) eqs 
33992  581 
)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

583 
 print_def is_pseudo_fun _ definer 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

585 
let 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

587 
concat [ 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

588 
(str o deresolve_classrel) (class, super_class), 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

589 
str "=", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

591 
]; 
52519
598addf65209
explicit hint for domain of class parameters in instance statements
haftmann
parents:
52435
diff
changeset

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

593 
concat [ 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

597 
]; 
33992  598 
in pair 
599 
(print_val_decl print_dicttypscheme 

55150  600 
(Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) 
33992  601 
(concat ( 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

602 
str definer 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

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

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

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

610 
str ":", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

611 
print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

614 
end; 
55681  615 
fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair 
55150  616 
[print_val_decl print_typscheme (Constant const, vs_ty)] 
33992  617 
((doublesemicolon o map str) ( 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

618 
"let" 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

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

622 
:: "failwith" 
68028  623 
@@ print_ocaml_string const 
33992  624 
)) 
55681  625 
 print_stmt _ (ML_Val binding) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

626 
let 
33992  627 
val (sig_p, p) = print_def (K false) true "let" binding 
628 
in pair 

629 
[sig_p] 

630 
(doublesemicolon [p]) 

631 
end 

55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

632 
 print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) = 
33992  633 
let 
634 
val print_def' = print_def (member (op =) pseudo_funs) false; 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

635 
fun print_pseudo_fun sym = concat [ 
29189  636 
str "let", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

637 
(str o deresolve) sym, 
29189  638 
str "=", 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

639 
(str o deresolve) sym, 
29189  640 
str "();;" 
641 
]; 

33992  642 
val (sig_ps, (ps, p)) = (apsnd split_last o split_list) 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

643 
(print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings); 
33992  644 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 
645 
in pair 

55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

646 
(map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE) 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

647 
((export :: map fst exports_bindings) ~~ sig_ps)) 
33992  648 
(Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps)) 
649 
end 

55681  650 
 print_stmt _ (ML_Datas [(tyco, (vs, []))]) = 
33992  651 
let 
55150  652 
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); 
33992  653 
in 
654 
pair 

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

55681  656 
(doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"]) 
33992  657 
end 
55681  658 
 print_stmt export (ML_Datas (data :: datas)) = 
28054  659 
let 
55681  660 
val decl_ps = print_datatype_decl "type" data 
33992  661 
:: map (print_datatype_decl "and") datas; 
55681  662 
val (ps, p) = split_last decl_ps; 
33992  663 
in pair 
55681  664 
(if Code_Namespace.is_public export 
665 
then decl_ps 

666 
else map (fn (tyco, (vs, _)) => 

667 
concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) 

668 
(data :: datas)) 

33992  669 
(Pretty.chunks (ps @ doublesemicolon [p])) 
670 
end 

55681  671 
 print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = 
28054  672 
let 
33992  673 
fun print_field s p = concat [str s, str ":", p]; 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

674 
fun print_super_class_field (classrel as (_, super_class)) = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

675 
print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); 
33992  676 
fun print_classparam_decl (classparam, ty) = 
677 
print_val_decl print_typscheme 

55150  678 
(Constant classparam, ([(v, [class])], ty)); 
33992  679 
fun print_classparam_field (classparam, ty) = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

680 
print_field (deresolve_const classparam) (print_typ NOBR ty); 
56812  681 
val w = "_" ^ Name.enforce_case true v; 
33992  682 
fun print_classparam_proj (classparam, _) = 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

683 
(concat o map str) ["let", deresolve_const classparam, w, "=", 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

684 
w ^ "." ^ deresolve_const classparam ^ ";;"]; 
33992  685 
val type_decl_p = concat [ 
55682  686 
str "type", 
687 
print_dicttyp (class, ITyVar v), 

28054  688 
str "=", 
33992  689 
enum_default "unit" ";" "{" "}" ( 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

690 
map print_super_class_field classrels 
33992  691 
@ map print_classparam_field classparams 
692 
) 

28054  693 
]; 
33992  694 
in pair 
71798
fc4f9dad5292
opaque export does not work as expected in presence of dependent instances
haftmann
parents:
70352
diff
changeset

695 
(if Code_Namespace.not_private export 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

696 
then type_decl_p :: map print_classparam_decl classparams 
66325
fd28cb6e6f2c
work around weakness in export calculation when generating OCaml code
haftmann
parents:
63303
diff
changeset

697 
else if null classrels andalso null classparams 
fd28cb6e6f2c
work around weakness in export calculation when generating OCaml code
haftmann
parents:
63303
diff
changeset

698 
then [type_decl_p] (*work around weakness in export calculation*) 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

699 
else [concat [str "type", print_dicttyp (class, ITyVar v)]]) 
33992  700 
(Pretty.chunks ( 
701 
doublesemicolon [type_decl_p] 

702 
:: map print_classparam_proj classparams 

703 
)) 

704 
end; 

705 
in print_stmt end; 

28054  706 

55677  707 
fun print_ocaml_module name decls body = 
38933
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38928
diff
changeset

708 
Pretty.chunks2 ( 
55677  709 
Pretty.chunks [ 
710 
str ("module " ^ name ^ " : sig"), 

711 
(indent 2 o Pretty.chunks) decls, 

712 
str "end = struct" 

713 
] 

33992  714 
:: body 
715 
@ str ("end;; (*struct " ^ name ^ "*)") 

28054  716 
); 
717 

28064  718 
val literals_ocaml = let 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

719 
fun numeral_ocaml k = if k < 0 
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

720 
then "(Z.neg " ^ numeral_ocaml (~ k) ^ ")" 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

721 
else if k <= 1073741823 
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

722 
then "(Z.of_int " ^ string_of_int k ^ ")" 
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

723 
else "(Z.of_string " ^ quote (string_of_int k) ^ ")" 
28064  724 
in Literals { 
68028  725 
literal_string = print_ocaml_string, 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

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

727 
literal_list = enum ";" "[" "]", 
28064  728 
infix_cons = (6, "::") 
729 
} end; 

730 

731 

28054  732 

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

734 

55681  735 
fun ml_program_of_program ctxt module_name reserved identifiers = 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

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

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

738 
let 
56826
ba18bd41e510
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents:
56812
diff
changeset

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

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

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

742 
let 
56826
ba18bd41e510
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
haftmann
parents:
56812
diff
changeset

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

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

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

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

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

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

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

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

751 
 namify_stmt (Code_Thingol.Classinst _) = namify_const false; 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

752 
fun ml_binding_of_stmt (sym as Constant const, (export, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _))) = 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

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

754 
val eqs = filter (snd o snd) raw_eqs; 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

756 
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

757 
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

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

760 
else (eqs, NONE) 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

761 
in ((export, ML_Function (const, (tysm, eqs'))), some_sym) end 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

762 
 ml_binding_of_stmt (sym as Class_Instance inst, (export, Code_Thingol.Classinst (stmt as { vs, ... }))) = 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

763 
((export, ML_Instance (inst, stmt)), 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

764 
if forall (null o snd) vs then SOME (sym, false) else NONE) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

765 
 ml_binding_of_stmt (sym, _) = 
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
51143
diff
changeset

766 
error ("Binding block containing illegal statement: " ^ 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

767 
Code_Symbol.quote ctxt sym) 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

768 
fun modify_fun (sym, (export, stmt)) = 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

769 
let 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

770 
val ((export', binding), some_value_sym) = ml_binding_of_stmt (sym, (export, stmt)); 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

771 
val ml_stmt = case binding 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

772 
of ML_Function (const, ((vs, ty), [])) => 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

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

774 
(length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

775 
 _ => case some_value_sym 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

776 
of NONE => ML_Funs ([(export', binding)], []) 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

777 
 SOME (sym, true) => ML_Funs ([(export, binding)], [sym]) 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

778 
 SOME (sym, false) => ML_Val binding 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

779 
in SOME (export, ml_stmt) end; 
39031  780 
fun modify_funs stmts = single (SOME 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

781 
(Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts > (apsnd o map_filter o Option.map) fst))) 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

782 
fun modify_datatypes stmts = 
63174
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

783 
let 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

784 
val datas = map_filter 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

785 
(fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt))  _ => NONE) stmts 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

786 
in 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

787 
if null datas then [] (*for abstract types wrt. code_reflect*) 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

788 
else datas 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

789 
> split_list 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

790 
> apfst Code_Namespace.join_exports 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

791 
> apsnd ML_Datas 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

792 
> SOME 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

793 
> single 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63024
diff
changeset

794 
end; 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

795 
fun modify_class stmts = 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

796 
the_single (map_filter 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

797 
(fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt))  _ => NONE) stmts) 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

798 
> apsnd ML_Class 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

799 
> SOME 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

800 
> single; 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

802 
if Code_Thingol.is_case stmt' then [] else [modify_fun stmt] 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

803 
 modify_stmts ((stmts as (_, (_, Code_Thingol.Fun _)) :: _)) = 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

804 
modify_funs (filter_out (Code_Thingol.is_case o snd o snd) stmts) 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

806 
modify_datatypes stmts 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

808 
modify_datatypes stmts 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

810 
modify_class stmts 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

812 
modify_class stmts 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

814 
modify_class stmts 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

816 
[modify_fun stmt] 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

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

819 
 modify_stmts stmts = error ("Illegal mutual dependencies: " ^ 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

820 
(Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts); 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

821 
in 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

822 
Code_Namespace.hierarchical_program ctxt { 
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
51143
diff
changeset

823 
module_name = module_name, reserved = reserved, identifiers = identifiers, 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

824 
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt, 
55776
7dd1971b39c1
amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
haftmann
parents:
55684
diff
changeset

825 
cyclic_modules = false, class_transitive = true, 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

826 
class_relation_public = true, empty_data = (), 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

827 
memorize_data = K I, modify_stmts = modify_stmts } 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

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

829 

69623
ef02c5e051e5
explicit model concerning files of generated code
haftmann
parents:
69207
diff
changeset

830 
fun serialize_ml print_ml_module print_ml_stmt ml_extension ctxt 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
55145
diff
changeset

831 
{ module_name, reserved_syms, identifiers, includes, 
69623
ef02c5e051e5
explicit model concerning files of generated code
haftmann
parents:
69207
diff
changeset

832 
class_syntax, tyco_syntax, const_syntax } program exports = 
28054  833 
let 
39147  834 

835 
(* build program *) 

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

836 
val { deresolver, hierarchical_program = ml_program } = 
55681  837 
ml_program_of_program ctxt module_name (Name.make_context reserved_syms) 
55683  838 
identifiers exports program; 
39147  839 

840 
(* print statements *) 

55679  841 
fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt 
47576  842 
tyco_syntax const_syntax (make_vars reserved_syms) 
55681  843 
(Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt 
844 
> apfst (fn decl => if Code_Namespace.not_private export then SOME decl else NONE); 

39147  845 

846 
(* print modules *) 

47576  847 
fun print_module _ base _ xs = 
39147  848 
let 
849 
val (raw_decls, body) = split_list xs; 

55677  850 
val decls = maps these raw_decls 
39147  851 
in (NONE, print_ml_module base decls body) end; 
852 

853 
(* serialization *) 

854 
val p = Pretty.chunks2 (map snd includes 

855 
@ map snd (Code_Namespace.print_hierarchical { 

856 
print_module = print_module, print_stmt = print_stmt, 

857 
lift_markup = apsnd } ml_program)); 

28054  858 
in 
69623
ef02c5e051e5
explicit model concerning files of generated code
haftmann
parents:
69207
diff
changeset

859 
(Code_Target.Singleton (ml_extension, p), try (deresolver [])) 
28054  860 
end; 
861 

38966  862 
val serializer_sml : Code_Target.serializer = 
69623
ef02c5e051e5
explicit model concerning files of generated code
haftmann
parents:
69207
diff
changeset

863 
Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt "ML"); 
28054  864 

38966  865 
val serializer_ocaml : Code_Target.serializer = 
69623
ef02c5e051e5
explicit model concerning files of generated code
haftmann
parents:
69207
diff
changeset

866 
Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt "ocaml"); 
28054  867 

38966  868 

869 
(** Isar setup **) 

870 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

871 
fun fun_syntax print_typ fxy [ty1, ty2] = 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

872 
brackify_infix (1, R) fxy ( 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

873 
print_typ (INFX (1, X)) ty1, 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

874 
str ">", 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

875 
print_typ (INFX (1, R)) ty2 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

876 
); 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

877 

59323  878 
val _ = Theory.setup 
879 
(Code_Target.add_language 

67207
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66326
diff
changeset

880 
(target_SML, {serializer = serializer_sml, literals = literals_sml, 
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66326
diff
changeset

881 
check = {env_var = "", 
41940  882 
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

883 
make_command = fn _ => 
67207
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66326
diff
changeset

884 
"isabelle process e 'datatype ref = datatype Unsynchronized.ref' f 'ROOT.ML' l Pure"}, 
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66326
diff
changeset

885 
evaluation_args = []}) 
59104  886 
#> Code_Target.add_language 
67207
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66326
diff
changeset

887 
(target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml, 
70352  888 
check = {env_var = "ISABELLE_OCAMLFIND", 
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

889 
make_destination = fn p => Path.append p (Path.explode "ROOT.ml") 
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

890 
(*extension demanded by OCaml compiler*), 
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

891 
make_command = fn _ => 
69950  892 
"\"$ISABELLE_OCAMLFIND\" ocamlopt w pu package zarith linkpkg ROOT.ml </dev/null"}, 
67207
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66326
diff
changeset

893 
evaluation_args = []}) 
55150  894 
#> Code_Target.set_printings (Type_Constructor ("fun", 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52138
diff
changeset

895 
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))])) 
28054  896 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
897 
#> fold (Code_Target.add_reserved target_SML) 

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

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

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

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

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

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

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

907 
"virtual", "when", "while", "with" 

908 
] 

69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69743
diff
changeset

909 
#> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Z"]); 
28054  910 

911 
end; (*struct*) 