author  haftmann 
Wed, 28 Jan 2015 08:29:08 +0100  
changeset 59456  180555df34ea 
parent 59323  468bd3aedfa1 
child 61129  774752af4a1f 
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 

59456
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

54 
fun print_char_any_ml s = 
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

55 
if Symbol.is_char s then ML_Syntax.print_char s else "\\092" ^ unprefix "\\" s; 
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

56 

180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

57 
val print_string_any_ml = quote o implode o map print_char_any_ml o Symbol.explode; 
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

58 

50625  59 
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve = 
28054  60 
let 
55150  61 
val deresolve_const = deresolve o Constant; 
62 
val deresolve_class = deresolve o Type_Class; 

63 
val deresolve_classrel = deresolve o Class_Relation; 

64 
val deresolve_inst = deresolve o Class_Instance; 

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

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

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

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

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

69 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] 
38923  70 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
55150  71 
of NONE => print_tyco_expr (Type_Constructor tyco, tys) 
47609  72 
 SOME (_, print) => print print_typ fxy tys) 
33992  73 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 
55150  74 
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

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

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

79 
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

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

81 
 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

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

83 
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

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

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

86 
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

87 
((str o deresolve_inst) inst :: 
55150  88 
(if is_pseudo_fun (Class_Instance inst) then [str "()"] 
33992  89 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

90 
 print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = 
56812  91 
[str (if k = 1 then Name.enforce_case true v ^ "_" 
92 
else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")] 

38922  93 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  94 
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

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

96 
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

97 
print_app is_pseudo_fun some_thm vars fxy (const, []) 
35228  98 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 
31889  99 
str "_" 
35228  100 
 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

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

104 
of SOME app => print_app is_pseudo_fun some_thm vars fxy app 
35228  105 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 
106 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

28054  108 
let 
31874  109 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
33992  110 
fun print_abs (pat, ty) = 
35228  111 
print_bind is_pseudo_fun some_thm NOBR pat 
28054  112 
#>> (fn p => concat [str "fn", p, str "=>"]); 
33992  113 
val (ps, vars') = fold_map print_abs binds vars; 
35228  114 
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

115 
 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

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

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

119 
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

120 
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

121 
 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

122 
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

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

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

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

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

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

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

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

137 
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

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

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

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

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

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

152 
str "end" 
28054  153 
] 
154 
end 

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

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

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

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

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

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

172 
[str "val", str (deresolve sym), str ":", print_typscheme typscheme]; 
33992  173 
fun print_datatype_decl definer (tyco, (vs, cos)) = 
174 
let 

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

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

176 
 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

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

180 
str definer 

55150  181 
:: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) 
33992  182 
:: str "=" 
183 
:: separate (str "") (map print_co cos) 

184 
) 

185 
end; 

186 
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

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

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

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

192 
> 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

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

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

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

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

197 
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

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

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

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

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

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

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

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

211 
in pair 

55150  212 
(print_val_decl print_typscheme (Constant const, vs_ty)) 
33992  213 
((Pretty.block o Pretty.fbreaks o shift) ( 
214 
print_eqn definer eq 

215 
:: map (print_eqn "") eqs 

216 
)) 

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

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

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

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

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

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

225 
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

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

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

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

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

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

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

232 
]; 
33992  233 
in pair 
234 
(print_val_decl print_dicttypscheme 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

257 
:: "Fail" 
59456
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

258 
@@ print_string_any_ml const 
33992  259 
)) 
55681  260 
 print_stmt _ (ML_Val binding) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

264 
[sig_p] 

265 
(semicolon [p]) 

266 
end 

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

267 
 print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) = 
33992  268 
let 
269 
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

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

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

274 
(str o deresolve) sym, 
29189  275 
str "();" 
276 
]; 

33992  277 
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

278 
(print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings); 
33992  279 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 
280 
in pair 

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

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

282 
((export :: map fst exports_bindings) ~~ sig_ps)) 
33992  283 
(Pretty.chunks (ps @ semicolon [p] :: pseudo_ps)) 
284 
end 

55681  285 
 print_stmt _ (ML_Datas [(tyco, (vs, []))]) = 
33992  286 
let 
55150  287 
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); 
33992  288 
in 
289 
pair 

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

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

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

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

303 
(data :: datas)) 

33992  304 
(Pretty.chunks (ps @ semicolon [p])) 
305 
end 

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

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

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

311 
fun print_super_class_decl (classrel as (_, super_class)) = 
33992  312 
print_val_decl print_dicttypscheme 
55150  313 
(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

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

315 
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

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

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

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

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

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

325 
print_proj (deresolve_const classparam) 
33992  326 
(print_typscheme ([(v, [class])], ty)); 
327 
in pair 

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

55681  329 
:: (if Code_Namespace.is_public export 
330 
then map print_super_class_decl classrels 

331 
@ map print_classparam_decl classparams 

332 
else [])) 

33992  333 
(Pretty.chunks ( 
28054  334 
concat [ 
55681  335 
str "type", 
336 
print_dicttyp (class, ITyVar v), 

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

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

339 
map print_super_class_field classrels 
33992  340 
@ map print_classparam_field classparams 
28054  341 
) 
342 
] 

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

343 
:: map print_super_class_proj classrels 
33992  344 
@ map print_classparam_proj classparams 
345 
)) 

28054  346 
end; 
33992  347 
in print_stmt end; 
28054  348 

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

350 
Pretty.chunks2 ( 
55677  351 
Pretty.chunks [ 
352 
str ("structure " ^ name ^ " : sig"), 

353 
(indent 2 o Pretty.chunks) decls, 

354 
str "end = struct" 

355 
] 

33992  356 
:: body 
357 
@ str ("end; (*struct " ^ name ^ "*)") 

28054  358 
); 
359 

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

59456
180555df34ea
string printing conformant to both (S)ML and Isabelle/ML
haftmann
parents:
59323
diff
changeset

362 
literal_string = print_string_any_ml, 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34246
diff
changeset

363 
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

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

367 

28054  368 

369 
(** OCaml serializer **) 

370 

50625  371 
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve = 
28054  372 
let 
55150  373 
val deresolve_const = deresolve o Constant; 
374 
val deresolve_class = deresolve o Type_Class; 

375 
val deresolve_classrel = deresolve o Class_Relation; 

376 
val deresolve_inst = deresolve o Class_Instance; 

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

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

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

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

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

381 
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] 
38923  382 
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco 
55150  383 
of NONE => print_tyco_expr (Type_Constructor tyco, tys) 
47576  384 
 SOME (_, print) => print print_typ fxy tys) 
33992  385 
 print_typ fxy (ITyVar v) = str ("'" ^ v); 
55150  386 
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

387 
fun print_typscheme_prefix (vs, p) = enum " >" "" "" 
33992  388 
(map_filter (fn (v, sort) => 
389 
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @ p); 

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

391 
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

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

393 
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

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

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

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

397 
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

398 
brackify BR ((str o deresolve_inst) inst :: 
55150  399 
(if is_pseudo_fun (Class_Instance inst) then [str "()"] 
33992  400 
else map_filter (print_dicts is_pseudo_fun BR) dss)) 
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset

401 
 print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = 
56812  402 
str (if k = 1 then "_" ^ Name.enforce_case true v 
403 
else "_" ^ Name.enforce_case true v ^ string_of_int (i+1)) 

38922  404 
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); 
33992  405 
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

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

407 
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

408 
print_app is_pseudo_fun some_thm vars fxy (const, []) 
35228  409 
 print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = 
31889  410 
str "_" 
35228  411 
 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

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

415 
of SOME app => print_app is_pseudo_fun some_thm vars fxy app 
35228  416 
 NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, 
417 
print_term is_pseudo_fun some_thm vars BR t2]) 

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

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

423 
 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

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

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

427 
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

428 
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

429 
 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

430 
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

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

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

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

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

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

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

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

445 
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

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

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

449 
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); 
47576  450 
fun print_let ((pat, _), t) vars = 
28054  451 
vars 
35228  452 
> print_bind is_pseudo_fun some_thm NOBR pat 
28054  453 
>> (fn p => concat 
35228  454 
[str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) 
33992  455 
val (ps, vars') = fold_map print_let binds vars; 
31665  456 
in 
457 
brackify_block fxy (Pretty.chunks ps) [] 

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

460 
 print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = 
28054  461 
let 
33992  462 
fun print_select delim (pat, body) = 
28054  463 
let 
35228  464 
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; 
465 
in concat [str delim, p, str ">", print_term is_pseudo_fun some_thm vars' NOBR body] end; 

28054  466 
in 
31665  467 
brackets ( 
28054  468 
str "match" 
35228  469 
:: print_term is_pseudo_fun some_thm vars NOBR t 
33992  470 
:: print_select "with" clause 
471 
:: map (print_select "") clauses 

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

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

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

475 
[str "val", str (deresolve sym), str ":", print_typscheme typscheme]; 
33992  476 
fun print_datatype_decl definer (tyco, (vs, cos)) = 
477 
let 

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

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

479 
 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

480 
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; 
33992  481 
in 
482 
concat ( 

483 
str definer 

55150  484 
:: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) 
33992  485 
:: str "=" 
486 
:: separate (str "") (map print_co cos) 

487 
) 

488 
end; 

489 
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

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

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

495 
> 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

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

497 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  498 
(insert (op =)) ts []); 
499 
in concat [ 

38778  500 
(Pretty.block o commas) 
35228  501 
(map (print_term is_pseudo_fun some_thm vars NOBR) ts), 
28054  502 
str ">", 
35228  503 
print_term is_pseudo_fun some_thm vars NOBR t 
28054  504 
] end; 
35228  505 
fun print_eqns is_pseudo [((ts, t), (some_thm, _))] = 
28054  506 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

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

508 
> 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

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

510 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
28054  511 
(insert (op =)) ts []); 
512 
in 

513 
concat ( 

29189  514 
(if is_pseudo then [str "()"] 
35228  515 
else map (print_term is_pseudo_fun some_thm vars BR) ts) 
28054  516 
@ str "=" 
35228  517 
@@ print_term is_pseudo_fun some_thm vars NOBR t 
28054  518 
) 
519 
end 

33992  520 
 print_eqns _ ((eq as (([_], _), _)) :: eqs) = 
28054  521 
Pretty.block ( 
522 
str "=" 

523 
:: Pretty.brk 1 

524 
:: str "function" 

525 
:: Pretty.brk 1 

33992  526 
:: print_eqn eq 
28054  527 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  528 
o single o print_eqn) eqs 
28054  529 
) 
33992  530 
 print_eqns _ (eqs as eq :: eqs') = 
28054  531 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

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

533 
> 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

534 
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

535 
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs; 
28054  536 
in 
537 
Pretty.block ( 

538 
Pretty.breaks dummy_parms 

539 
@ Pretty.brk 1 

540 
:: str "=" 

541 
:: Pretty.brk 1 

542 
:: str "match" 

543 
:: Pretty.brk 1 

38778  544 
:: (Pretty.block o commas) dummy_parms 
28054  545 
:: Pretty.brk 1 
546 
:: str "with" 

547 
:: Pretty.brk 1 

33992  548 
:: print_eqn eq 
28054  549 
:: maps (append [Pretty.fbrk, str "", Pretty.brk 1] 
33992  550 
o single o print_eqn) eqs' 
28054  551 
) 
552 
end; 

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

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

554 
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

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

559 
prolog 
33992  560 
:: print_dict_args vs 
55150  561 
@ print_eqns (is_pseudo_fun (Constant const)) eqs 
33992  562 
)) 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

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

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

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

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

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

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

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

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

571 
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

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

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

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

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

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

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

578 
]; 
33992  579 
in pair 
580 
(print_val_decl print_dicttypscheme 

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

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

584 
:: (str o deresolve_inst) inst 
55150  585 
:: (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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

604 
@@ ML_Syntax.print_string const 
33992  605 
)) 
55681  606 
 print_stmt _ (ML_Val binding) = 
33636
a9bb3f063773
accomplish mutual recursion between fun and inst
haftmann
parents:
33519
diff
changeset

607 
let 
33992  608 
val (sig_p, p) = print_def (K false) true "let" binding 
609 
in pair 

610 
[sig_p] 

611 
(doublesemicolon [p]) 

612 
end 

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

613 
 print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) = 
33992  614 
let 
615 
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

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

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

620 
(str o deresolve) sym, 
29189  621 
str "();;" 
622 
]; 

33992  623 
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

624 
(print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings); 
33992  625 
val pseudo_ps = map print_pseudo_fun pseudo_funs; 
626 
in pair 

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

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

628 
((export :: map fst exports_bindings) ~~ sig_ps)) 
33992  629 
(Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps)) 
630 
end 

55681  631 
 print_stmt _ (ML_Datas [(tyco, (vs, []))]) = 
33992  632 
let 
55150  633 
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); 
33992  634 
in 
635 
pair 

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

55681  637 
(doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"]) 
33992  638 
end 
55681  639 
 print_stmt export (ML_Datas (data :: datas)) = 
28054  640 
let 
55681  641 
val decl_ps = print_datatype_decl "type" data 
33992  642 
:: map (print_datatype_decl "and") datas; 
55681  643 
val (ps, p) = split_last decl_ps; 
33992  644 
in pair 
55681  645 
(if Code_Namespace.is_public export 
646 
then decl_ps 

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

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

649 
(data :: datas)) 

33992  650 
(Pretty.chunks (ps @ doublesemicolon [p])) 
651 
end 

55681  652 
 print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = 
28054  653 
let 
33992  654 
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

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

656 
print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); 
33992  657 
fun print_classparam_decl (classparam, ty) = 
658 
print_val_decl print_typscheme 

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

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

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

665 
w ^ "." ^ deresolve_const classparam ^ ";;"]; 
33992  666 
val type_decl_p = concat [ 
55682  667 
str "type", 
668 
print_dicttyp (class, ITyVar v), 

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

671 
map print_super_class_field classrels 
33992  672 
@ map print_classparam_field classparams 
673 
) 

28054  674 
]; 
33992  675 
in pair 
55684
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

677 
then type_decl_p :: map print_classparam_decl classparams 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

678 
else [concat [str "type", print_dicttyp (class, ITyVar v)]]) 
33992  679 
(Pretty.chunks ( 
680 
doublesemicolon [type_decl_p] 

681 
:: map print_classparam_proj classparams 

682 
)) 

683 
end; 

684 
in print_stmt end; 

28054  685 

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

687 
Pretty.chunks2 ( 
55677  688 
Pretty.chunks [ 
689 
str ("module " ^ name ^ " : sig"), 

690 
(indent 2 o Pretty.chunks) decls, 

691 
str "end = struct" 

692 
] 

33992  693 
:: body 
694 
@ str ("end;; (*struct " ^ name ^ "*)") 

28054  695 
); 
696 

28064  697 
val literals_ocaml = let 
698 
fun chr i = 

699 
let 

700 
val xs = string_of_int i; 

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

701 
val ys = replicate_string (3  length (raw_explode xs)) "0"; 
28064  702 
in "\\" ^ ys ^ xs end; 
703 
fun char_ocaml c = 

704 
let 

705 
val i = ord c; 

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

707 
then chr i else c 

708 
in s end; 

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

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

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

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

712 
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

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

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

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

718 
literal_list = enum ";" "[" "]", 
28064  719 
infix_cons = (6, "::") 
720 
} end; 

721 

722 

28054  723 

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

725 

55681  726 
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

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

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

729 
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

730 
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

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

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

733 
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

734 
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

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

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

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

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

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

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

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

742 
 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

743 
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

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

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

746 
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

747 
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

748 
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

749 
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

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

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

752 
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

753 
 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

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

755 
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

756 
 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

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

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

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

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

761 
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

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

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

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

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

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

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

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

769 
 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

770 
in SOME (export, ml_stmt) end; 
39031  771 
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

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

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

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

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

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

777 
> apfst Code_Namespace.join_exports 
ee49b4f7edc8
keep only identifiers public which are explicitly requested or demanded by dependencies
haftmann
parents:
55683
diff
changeset

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

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

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

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

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

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

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

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

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

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

788 
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

789 
 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

790 
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

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

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

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

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

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

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

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

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

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

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

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

802 
[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.Classinst _)) :: _)) = 
39028
0dd6c5a0beef
use code_namespace module for SML and OCaml code
haftmann
parents:
38966
diff
changeset

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

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

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

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

808 
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

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

810 
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

811 
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

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

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

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

815 

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

817 
{ module_name, reserved_syms, identifiers, includes, 
55683  818 
class_syntax, tyco_syntax, const_syntax } exports program = 
28054  819 
let 
39147  820 

821 
(* build program *) 

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

822 
val { deresolver, hierarchical_program = ml_program } = 
55681  823 
ml_program_of_program ctxt module_name (Name.make_context reserved_syms) 
55683  824 
identifiers exports program; 
39147  825 

826 
(* print statements *) 

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

39147  831 

832 
(* print modules *) 

47576  833 
fun print_module _ base _ xs = 
39147  834 
let 
835 
val (raw_decls, body) = split_list xs; 

55677  836 
val decls = maps these raw_decls 
39147  837 
in (NONE, print_ml_module base decls body) end; 
838 

839 
(* serialization *) 

840 
val p = Pretty.chunks2 (map snd includes 

841 
@ map snd (Code_Namespace.print_hierarchical { 

842 
print_module = print_module, print_stmt = print_stmt, 

843 
lift_markup = apsnd } ml_program)); 

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

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

846 
fun prepare syms width p = ([("", format syms width p)], try (deresolver [])); 
28054  847 
in 
48568  848 
Code_Target.serialization write prepare p 
28054  849 
end; 
850 

38966  851 
val serializer_sml : Code_Target.serializer = 
55677  852 
Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt); 
28054  853 

38966  854 
val serializer_ocaml : Code_Target.serializer = 
55677  855 
Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt); 
28054  856 

38966  857 

858 
(** Isar setup **) 

859 

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

860 
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

861 
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

862 
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

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

864 
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

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

866 

59323  867 
val _ = Theory.setup 
868 
(Code_Target.add_language 

38966  869 
(target_SML, { serializer = serializer_sml, literals = literals_sml, 
41940  870 
check = { env_var = "ISABELLE_PROCESS", 
871 
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

872 
make_command = fn _ => 
51091
c007c6bf4a35
another attempt for a uniform abort on code generation errors
haftmann
parents:
50625
diff
changeset

873 
"\"$ISABELLE_PROCESS\" r q e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } }) 
59104  874 
#> Code_Target.add_language 
38966  875 
(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

876 
check = { env_var = "ISABELLE_OCAML", 
41940  877 
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

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

880 
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))])) 
28054  881 
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names 
882 
#> fold (Code_Target.add_reserved target_SML) 

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

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

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

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

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

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

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

892 
"virtual", "when", "while", "with" 

893 
] 

59323  894 
#> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]); 
28054  895 

896 
end; (*struct*) 