author  haftmann 
Mon, 30 Aug 2010 16:31:38 +0200  
changeset 38915  026526cba0e6 
parent 38913  d1d4d808be26 
child 38916  c0b857a04758 
permissions  rwrr 
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37669
diff
changeset

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

4 
Serializer for Haskell. 

5 
*) 

6 

7 
signature CODE_HASKELL = 

8 
sig 

37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37669
diff
changeset

9 
val target: string 
28054  10 
val setup: theory > theory 
11 
end; 

12 

13 
structure Code_Haskell : CODE_HASKELL = 

14 
struct 

15 

16 
val target = "Haskell"; 

17 

18 
open Basic_Code_Thingol; 

19 
open Code_Printer; 

20 

21 
infixr 5 @@; 

22 
infixr 5 @; 

23 

24 

25 
(** Haskell serializer **) 

26 

33991  27 
fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

28 
reserved deresolve contr_classparam_typs deriving_show = 
28054  29 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

30 
val deresolve_base = Long_Name.base_name o deresolve; 
28054  31 
fun class_name class = case syntax_class class 
32 
of NONE => deresolve class 

28687  33 
 SOME class => class; 
33991  34 
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs 
28054  35 
of [] => [] 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

36 
 constraints => enum "," "(" ")" ( 
28054  37 
map (fn (v, class) => 
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37242
diff
changeset

38 
str (class_name class ^ " " ^ lookup_var tyvars v)) constraints) 
28054  39 
@@ str " => "; 
33991  40 
fun print_typforall tyvars vs = case map fst vs 
28054  41 
of [] => [] 
42 
 vnames => str "forall " :: Pretty.breaks 

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

43 
(map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; 
33991  44 
fun print_tyco_expr tyvars fxy (tyco, tys) = 
45 
brackify fxy (str tyco :: map (print_typ tyvars BR) tys) 

46 
and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco 

47 
of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) 

48 
 SOME (i, print) => print (print_typ tyvars) fxy tys) 

49 
 print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; 

50 
fun print_typdecl tyvars (vs, tycoexpr) = 

51 
Pretty.block (print_typcontext tyvars vs @ print_tyco_expr tyvars NOBR tycoexpr); 

52 
fun print_typscheme tyvars (vs, ty) = 

53 
Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @ print_typ tyvars NOBR ty); 

35228  54 
fun print_term tyvars some_thm vars fxy (IConst c) = 
55 
print_app tyvars some_thm vars fxy (c, []) 

56 
 print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) = 

28054  57 
(case Code_Thingol.unfold_const_app t 
35228  58 
of SOME app => print_app tyvars some_thm vars fxy app 
28054  59 
 _ => 
60 
brackify fxy [ 

35228  61 
print_term tyvars some_thm vars NOBR t1, 
62 
print_term tyvars some_thm vars BR t2 

28054  63 
]) 
35228  64 
 print_term tyvars some_thm vars fxy (IVar NONE) = 
31889  65 
str "_" 
35228  66 
 print_term tyvars 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

67 
(str o lookup_var vars) v 
35228  68 
 print_term tyvars some_thm vars fxy (t as _ `=> _) = 
28054  69 
let 
31874  70 
val (binds, t') = Code_Thingol.unfold_pat_abs t; 
35228  71 
val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; 
72 
in brackets (str "\\" :: ps @ str ">" @@ print_term tyvars some_thm vars' NOBR t') end 

73 
 print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) = 

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

35228  76 
then print_case tyvars some_thm vars fxy cases 
77 
else print_app tyvars some_thm vars fxy c_ts 

78 
 NONE => print_case tyvars some_thm vars fxy cases) 

37449  79 
and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c 
35228  80 
of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts 
28054  81 
 fingerprint => let 
33957  82 
val ts_fingerprint = ts ~~ take (length ts) fingerprint; 
28054  83 
val needs_annotation = forall (fn (_, NONE) => true  (t, SOME _) => 
84 
(not o Code_Thingol.locally_monomorphic) t) ts_fingerprint; 

35228  85 
fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t 
33991  86 
 print_term_anno (t, SOME _) ty = 
35228  87 
brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty]; 
28054  88 
in 
89 
if needs_annotation then 

37449  90 
(str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs) 
35228  91 
else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts 
28054  92 
end 
33991  93 
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const 
35228  94 
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p 
95 
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = 

28054  96 
let 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29832
diff
changeset

97 
val (binds, body) = Code_Thingol.unfold_let (ICase cases); 
33991  98 
fun print_match ((pat, ty), t) vars = 
28054  99 
vars 
35228  100 
> print_bind tyvars some_thm BR pat 
101 
>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) 

33991  102 
val (ps, vars') = fold_map print_match binds vars; 
31665  103 
in brackify_block fxy (str "let {") 
104 
ps 

35228  105 
(concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body]) 
28054  106 
end 
35228  107 
 print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) = 
28054  108 
let 
33991  109 
fun print_select (pat, body) = 
28054  110 
let 
35228  111 
val (p, vars') = print_bind tyvars some_thm NOBR pat vars; 
112 
in semicolon [p, str ">", print_term tyvars some_thm vars' NOBR body] end; 

36576  113 
in Pretty.block_enclose 
114 
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})") 

33991  115 
(map print_select clauses) 
28054  116 
end 
35228  117 
 print_case tyvars some_thm vars fxy ((_, []), _) = 
31376  118 
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; 
37437  119 
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = 
28054  120 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

121 
val tyvars = intro_vars (map fst vs) reserved; 
34269  122 
fun print_err n = 
33991  123 
semicolon ( 
28054  124 
(str o deresolve_base) name 
125 
:: map str (replicate n "_") 

126 
@ str "=" 

127 
:: str "error" 

33991  128 
@@ (str o ML_Syntax.print_string 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

129 
o Long_Name.base_name o Long_Name.qualifier) name 
34269  130 
); 
35228  131 
fun print_eqn ((ts, t), (some_thm, _)) = 
28054  132 
let 
32913  133 
val consts = fold Code_Thingol.add_constnames (t :: ts) []; 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

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

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

137 
> intro_vars ((fold o Code_Thingol.fold_varnames) 
32925  138 
(insert (op =)) ts []); 
28054  139 
in 
140 
semicolon ( 

141 
(str o deresolve_base) name 

35228  142 
:: map (print_term tyvars some_thm vars BR) ts 
28054  143 
@ str "=" 
35228  144 
@@ print_term tyvars some_thm vars NOBR t 
28054  145 
) 
146 
end; 

147 
in 

148 
Pretty.chunks ( 

33991  149 
semicolon [ 
28054  150 
(str o suffix " ::" o deresolve_base) name, 
33991  151 
print_typscheme tyvars (vs, ty) 
28054  152 
] 
34269  153 
:: (case filter (snd o snd) raw_eqs 
154 
of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)] 

155 
 eqs => map print_eqn eqs) 

28054  156 
) 
157 
end 

33991  158 
 print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = 
28054  159 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

160 
val tyvars = intro_vars (map fst vs) reserved; 
28054  161 
in 
162 
semicolon [ 

163 
str "data", 

33991  164 
print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) 
28054  165 
] 
166 
end 

37449  167 
 print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) = 
28054  168 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

169 
val tyvars = intro_vars (map fst vs) reserved; 
28054  170 
in 
171 
semicolon ( 

172 
str "newtype" 

33991  173 
:: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) 
28054  174 
:: str "=" 
175 
:: (str o deresolve_base) co 

33991  176 
:: print_typ tyvars BR ty 
28054  177 
:: (if deriving_show name then [str "deriving (Read, Show)"] else []) 
178 
) 

179 
end 

33991  180 
 print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = 
28054  181 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

182 
val tyvars = intro_vars (map fst vs) reserved; 
37449  183 
fun print_co ((co, _), tys) = 
28054  184 
concat ( 
185 
(str o deresolve_base) co 

33991  186 
:: map (print_typ tyvars BR) tys 
28054  187 
) 
188 
in 

189 
semicolon ( 

190 
str "data" 

33991  191 
:: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) 
28054  192 
:: str "=" 
33991  193 
:: print_co co 
194 
:: map ((fn p => Pretty.block [str " ", p]) o print_co) cos 

28054  195 
@ (if deriving_show name then [str "deriving (Read, Show)"] else []) 
196 
) 

197 
end 

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

198 
 print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) = 
28054  199 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

200 
val tyvars = intro_vars [v] reserved; 
33991  201 
fun print_classparam (classparam, ty) = 
28054  202 
semicolon [ 
28687  203 
(str o deresolve_base) classparam, 
28054  204 
str "::", 
33991  205 
print_typ tyvars NOBR ty 
28054  206 
] 
207 
in 

208 
Pretty.block_enclose ( 

209 
Pretty.block [ 

210 
str "class ", 

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

211 
Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]), 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

212 
str (deresolve_base name ^ " " ^ lookup_var tyvars v), 
28054  213 
str " where {" 
214 
], 

215 
str "};" 

33991  216 
) (map print_classparam classparams) 
28054  217 
end 
37449  218 
 print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) = 
28054  219 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

220 
val tyvars = intro_vars (map fst vs) reserved; 
37881  221 
fun requires_args classparam = case syntax_const classparam 
222 
of NONE => 0 

223 
 SOME (Code_Printer.Plain_const_syntax _) => 0 

224 
 SOME (Code_Printer.Complex_const_syntax (k,_ )) => k; 

225 
fun print_classparam_instance ((classparam, const), (thm, _)) = 

226 
case requires_args classparam 

227 
of 0 => semicolon [ 

228 
(str o deresolve_base) classparam, 

28687  229 
str "=", 
37881  230 
print_app tyvars (SOME thm) reserved NOBR (const, []) 
28687  231 
] 
37881  232 
 k => 
233 
let 

234 
val (c, (_, tys)) = const; 

235 
val (vs, rhs) = (apfst o map) fst 

236 
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); 

237 
val s = if (is_some o syntax_const) c 

238 
then NONE else (SOME o Long_Name.base_name o deresolve) c; 

239 
val vars = reserved 

240 
> intro_vars (map_filter I (s :: vs)); 

241 
val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; 

242 
(*dictionaries are not relevant at this late stage*) 

243 
in 

244 
semicolon [ 

245 
print_term tyvars (SOME thm) vars NOBR lhs, 

246 
str "=", 

247 
print_term tyvars (SOME thm) vars NOBR rhs 

248 
] 

249 
end; 

28054  250 
in 
251 
Pretty.block_enclose ( 

252 
Pretty.block [ 

253 
str "instance ", 

33991  254 
Pretty.block (print_typcontext tyvars vs), 
28054  255 
str (class_name class ^ " "), 
33991  256 
print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), 
28054  257 
str " where {" 
258 
], 

259 
str "};" 

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

260 
) (map print_classparam_instance classparam_instances) 
28054  261 
end; 
33991  262 
in print_stmt end; 
28054  263 

38779  264 
fun haskell_program_of_program labelled_name module_prefix reserved module_alias program = 
28054  265 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

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

267 
val mk_name_module = mk_name_module reserved module_prefix module_alias program; 
28054  268 
fun add_stmt (name, (stmt, deps)) = 
269 
let 

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

270 
val (module_name, base) = dest_name name; 
28054  271 
val module_name' = mk_name_module module_name; 
272 
val mk_name_stmt = yield_singleton Name.variants; 

273 
fun add_fun upper (nsp_fun, nsp_typ) = 

274 
let 

275 
val (base', nsp_fun') = 

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

276 
mk_name_stmt (if upper then first_upper base else base) nsp_fun 
28054  277 
in (base', (nsp_fun', nsp_typ)) end; 
278 
fun add_typ (nsp_fun, nsp_typ) = 

279 
let 

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

280 
val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ 
28054  281 
in (base', (nsp_fun, nsp_typ')) end; 
282 
val add_name = case stmt 

37439  283 
of Code_Thingol.Fun (_, (_, SOME _)) => pair base 
284 
 Code_Thingol.Fun _ => add_fun false 

28054  285 
 Code_Thingol.Datatype _ => add_typ 
286 
 Code_Thingol.Datatypecons _ => add_fun true 

287 
 Code_Thingol.Class _ => add_typ 

288 
 Code_Thingol.Classrel _ => pair base 

289 
 Code_Thingol.Classparam _ => add_fun false 

290 
 Code_Thingol.Classinst _ => pair base; 

291 
fun add_stmt' base' = case stmt 

37439  292 
of Code_Thingol.Fun (_, (_, SOME _)) => 
293 
I 

294 
 Code_Thingol.Datatypecons _ => 

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

295 
cons (name, (Long_Name.append module_name' base', NONE)) 
28054  296 
 Code_Thingol.Classrel _ => I 
297 
 Code_Thingol.Classparam _ => 

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

298 
cons (name, (Long_Name.append module_name' base', NONE)) 
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

299 
 _ => cons (name, (Long_Name.append module_name' base', SOME stmt)); 
28054  300 
in 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

301 
Symtab.map_default (module_name', ([], ([], (reserved, reserved)))) 
28054  302 
(apfst (fold (insert (op = : string * string > bool)) deps)) 
303 
#> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name')) 

304 
#> (fn (base', names) => 

305 
(Symtab.map_entry module_name' o apsnd) (fn (stmts, _) => 

306 
(add_stmt' base' stmts, names))) 

307 
end; 

308 
val hs_program = fold add_stmt (AList.make (fn name => 

309 
(Graph.get_node program name, Graph.imm_succs program name)) 

310 
(Graph.strong_conn program > flat)) Symtab.empty; 

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

311 
fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

312 
o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

313 
handle Option => error ("Unknown statement name: " ^ labelled_name name); 
28054  314 
in (deresolver, hs_program) end; 
315 

38779  316 
fun serialize_haskell module_prefix module_name string_classes labelled_name 
317 
raw_reserved includes module_alias 

38912  318 
syntax_class syntax_tyco syntax_const program 
38913  319 
(stmt_names, presentation_stmt_names) = 
28054  320 
let 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

321 
val reserved = fold (insert (op =) o fst) includes raw_reserved; 
28054  322 
val (deresolver, hs_program) = haskell_program_of_program labelled_name 
38779  323 
module_prefix reserved module_alias program; 
28054  324 
val contr_classparam_typs = Code_Thingol.contr_classparam_typs program; 
325 
fun deriving_show tyco = 

326 
let 

327 
fun deriv _ "fun" = false 

34085  328 
 deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco) 
329 
andalso (member (op =) tycos tyco 

330 
orelse case try (Graph.get_node program) tyco 

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

331 
of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos)) 
28054  332 
(maps snd cs) 
34085  333 
 NONE => true) 
28054  334 
and deriv' tycos (tyco `%% tys) = deriv tycos tyco 
335 
andalso forall (deriv' tycos) tys 

336 
 deriv' _ (ITyVar _) = true 

337 
in deriv [] tyco end; 

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

338 
val reserved = make_vars reserved; 
33991  339 
fun print_stmt qualified = print_haskell_stmt labelled_name 
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset

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

341 
(if qualified then deresolver else Long_Name.base_name o deresolver) 
32903  342 
contr_classparam_typs 
28054  343 
(if string_classes then deriving_show else K false); 
33991  344 
fun print_module name content = 
38768  345 
(name, Pretty.chunks2 [ 
28054  346 
str ("module " ^ name ^ " where {"), 
347 
content, 

348 
str "}" 

349 
]); 

350 
fun serialize_module1 (module_name', (deps, (stmts, _))) = 

351 
let 

352 
val stmt_names = map fst stmts; 

33421
3789fe962a08
always be qualified  suspected smartness in fact never worked as expected
haftmann
parents:
32925
diff
changeset

353 
val qualified = is_none module_name; 
3789fe962a08
always be qualified  suspected smartness in fact never worked as expected
haftmann
parents:
32925
diff
changeset

354 
val imports = subtract (op =) stmt_names deps 
28054  355 
> distinct (op =) 
33421
3789fe962a08
always be qualified  suspected smartness in fact never worked as expected
haftmann
parents:
32925
diff
changeset

356 
> map_filter (try deresolver) 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

357 
> map Long_Name.qualifier 
28054  358 
> distinct (op =); 
33991  359 
fun print_import_include (name, _) = str ("import qualified " ^ name ^ ";"); 
34049  360 
fun print_import_module name = str ((if qualified 
361 
then "import qualified " 

362 
else "import ") ^ name ^ ";"); 

33991  363 
val import_ps = map print_import_include includes @ map print_import_module imports 
34073
7b0bf55adecd
repaired accident: do not forget module contents if there are no imports
haftmann
parents:
34049
diff
changeset

364 
val content = Pretty.chunks2 ((if null import_ps then [] else [Pretty.chunks import_ps]) 
33991  365 
@ map_filter 
366 
(fn (name, (_, SOME stmt)) => SOME (print_stmt qualified (name, stmt)) 

367 
 (_, (_, NONE)) => NONE) stmts 

368 
); 

369 
in print_module module_name' content end; 

370 
fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter 

36535  371 
(fn (name, (_, SOME stmt)) => if null presentation_stmt_names 
372 
orelse member (op =) presentation_stmt_names name 

33991  373 
then SOME (print_stmt false (name, stmt)) 
28054  374 
else NONE 
33991  375 
 (_, (_, NONE)) => NONE) stmts); 
28054  376 
val serialize_module = 
36535  377 
if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2; 
38915  378 
fun write_module width (SOME destination) (modlname, content) = 
379 
let 

380 
val _ = File.check destination; 

381 
val filename = case modlname 

382 
of "" => Path.explode "Main.hs" 

383 
 _ => (Path.ext "hs" o Path.explode o implode o separate "/" 

384 
o Long_Name.explode) modlname; 

385 
val pathname = Path.append destination filename; 

386 
val _ = File.mkdir_leaf (Path.dir pathname); 

387 
in File.write pathname 

388 
("{# OPTIONS_GHC fglasgowexts #}\n\n" 

389 
^ string_of_pretty width content) 

390 
end 

391 
 write_module width NONE (_, content) = writeln_pretty width content; 

28054  392 
in 
38910  393 
Code_Target.mk_serialization 
38915  394 
(fn width => fn destination => K () o map (write_module width destination)) 
395 
(fn width => rpair [] o cat_lines o map (string_of_pretty width o snd)) 

33991  396 
(map (uncurry print_module) includes 
28054  397 
@ map serialize_module (Symtab.dest hs_program)) 
398 
end; 

399 

28064  400 
val literals = let 
401 
fun char_haskell c = 

402 
let 

403 
val s = ML_Syntax.print_char c; 

404 
in if s = "'" then "\\'" else s end; 

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

405 
fun numeral_haskell k = if k >= 0 then string_of_int k 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34269
diff
changeset

406 
else Library.enclose "(" ")" (signed_string_of_int k); 
28064  407 
in Literals { 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34085
diff
changeset

408 
literal_char = Library.enclose "'" "'" o char_haskell, 
28064  409 
literal_string = quote o translate_string char_haskell, 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34269
diff
changeset

410 
literal_numeral = numeral_haskell, 
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34269
diff
changeset

411 
literal_positive_numeral = numeral_haskell, 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37881
diff
changeset

412 
literal_alternative_numeral = numeral_haskell, 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34269
diff
changeset

413 
literal_naive_numeral = numeral_haskell, 
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34085
diff
changeset

414 
literal_list = enum "," "[" "]", 
28064  415 
infix_cons = (5, ":") 
416 
} end; 

417 

28054  418 

419 
(** optional monad syntax **) 

420 

421 
fun pretty_haskell_monad c_bind = 

422 
let 

31874  423 
fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2 
31889  424 
of SOME ((pat, ty), t') => 
425 
SOME ((SOME ((pat, ty), true), t1), t') 

28145  426 
 NONE => NONE; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

427 
fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

428 
if c = c_bind_name then dest_bind t1 t2 
28145  429 
else NONE 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

430 
 dest_monad _ t = case Code_Thingol.split_let t 
28145  431 
of SOME (((pat, ty), tbind), t') => 
31889  432 
SOME ((SOME ((pat, ty), false), tbind), t') 
28145  433 
 NONE => NONE; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28350
diff
changeset

434 
fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name); 
33991  435 
fun print_monad print_bind print_term (NONE, t) vars = 
436 
(semicolon [print_term vars NOBR t], vars) 

437 
 print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars 

438 
> print_bind NOBR bind 

439 
>> (fn p => semicolon [p, str "<", print_term vars NOBR t]) 

440 
 print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars 

441 
> print_bind NOBR bind 

37832  442 
>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]); 
33991  443 
fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 
28145  444 
of SOME (bind, t') => let 
31054  445 
val (binds, t'') = implode_monad c_bind' t' 
33991  446 
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) 
447 
(bind :: binds) vars; 

448 
in 

37833
1381665d9550
more consistent spacing in generated monadic code
haftmann
parents:
37832
diff
changeset

449 
(brackify fxy o single o enclose "do { " " }" o Pretty.breaks) 
33991  450 
(ps @ print_term vars' NOBR t'') 
451 
end 

28145  452 
 NONE => brackify_infix (1, L) fxy 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36960
diff
changeset

453 
(print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) 
31054  454 
in (2, ([c_bind], pretty)) end; 
28054  455 

28145  456 
fun add_monad target' raw_c_bind thy = 
28054  457 
let 
31156  458 
val c_bind = Code.read_const thy raw_c_bind; 
28054  459 
in if target = target' then 
460 
thy 

28145  461 
> Code_Target.add_syntax_const target c_bind 
37881  462 
(SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind))) 
28054  463 
else error "Only Haskell target allows for monad syntax" end; 
464 

465 

466 
(** Isar setup **) 

467 

37821  468 
fun isar_serializer module_name = 
28054  469 
Code_Target.parse_args (Scan.option (Args.$$$ "root"  Args.colon  Args.name) 
470 
 Scan.optional (Args.$$$ "string_classes" >> K true) false 

471 
>> (fn (module_prefix, string_classes) => 

33991  472 
serialize_haskell module_prefix module_name string_classes)); 
28054  473 

474 
val _ = 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36576
diff
changeset

475 
Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl ( 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36576
diff
changeset

476 
Parse.term_group  Parse.name >> (fn (raw_bind, target) => 
28145  477 
Toplevel.theory (add_monad target raw_bind)) 
28054  478 
); 
479 

480 
val setup = 

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

482 
(target, { serializer = isar_serializer, literals = literals, 
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

483 
check = { env_var = "EXEC_GHC", make_destination = I, 
38863
9070a7c356c9
code checking: compiler invocation happens in same directory as generated file  avoid problem with different path representations on cygwin
haftmann
parents:
38779
diff
changeset

484 
make_command = fn ghc => fn module_name => 
37822
cf3588177676
use generic description slot for formal code checking
haftmann
parents:
37821
diff
changeset

485 
ghc ^ " fglasgowexts odir build hidir build stubdir build e \"\" " ^ module_name ^ ".hs" } }) 
33991  486 
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36960
diff
changeset

487 
brackify_infix (1, R) fxy ( 
33991  488 
print_typ (INFX (1, X)) ty1, 
28054  489 
str ">", 
33991  490 
print_typ (INFX (1, R)) ty2 
37242
97097e589715
brackify_infix etc.: no break before infix operator  eases survival in Scala
haftmann
parents:
36960
diff
changeset

491 
))) 
28054  492 
#> fold (Code_Target.add_reserved target) [ 
493 
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", 

494 
"import", "default", "forall", "let", "in", "class", "qualified", "data", 

495 
"newtype", "instance", "if", "then", "else", "type", "as", "do", "module" 

496 
] 

497 
#> fold (Code_Target.add_reserved target) [ 

498 
"Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int", 

499 
"Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded", 

500 
"Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor", 

501 
"AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException", 

502 
"BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException", 

503 
"Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure", 

504 
"ExitSuccess", "False", "GT", "HeapOverflow", 

505 
"IOError", "IOException", "IllegalOperation", 

506 
"IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError", 

507 
"NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow", 

508 
"PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError", 

509 
"RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow", 

510 
"ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow", 

511 
"UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all", 

512 
"and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan", 

513 
"atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen", 

514 
"boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break", 

515 
"catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const", 

516 
"cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod", 

517 
"doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem", 

518 
"emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo", 

519 
"enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip", 

520 
"floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational", 

521 
"floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble", 

522 
"fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj", 

523 
"fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head", 

524 
"id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha", 

525 
"isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite", 

526 
"isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'", 

527 
"last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log", 

528 
"logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum", 

529 
"maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem", 

530 
"null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo", 

531 
"numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 

532 
"print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn", 

533 
"quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat", 

534 
"rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile", 

535 
"readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn", 

536 
"readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational", 

537 
"realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse", 

538 
"round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence", 

539 
"sequence_", "show", "showChar", "showException", "showField", "showList", 

540 
"showLitChar", "showParen", "showString", "shows", "showsPrec", "significand", 

541 
"signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract", 

542 
"succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult", 

543 
"throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry", 

544 
"undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords", 

545 
"unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3" 

546 
] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*); 

547 

548 
end; (*struct*) 