changeset 27103 | d8549f4d900b |
parent 27024 | fcab2dd46872 |
child 27304 | 720c8115d723 |
27102:a98cd7450204 | 27103:d8549f4d900b |
---|---|
26 val add_pretty_numeral: string -> bool -> bool -> string -> string -> string |
26 val add_pretty_numeral: string -> bool -> bool -> string -> string -> string |
27 -> string -> string -> theory -> theory; |
27 -> string -> string -> theory -> theory; |
28 val add_pretty_message: string -> string -> string list -> string |
28 val add_pretty_message: string -> string -> string list -> string |
29 -> string -> string -> theory -> theory; |
29 -> string -> string -> theory -> theory; |
30 |
30 |
31 val allow_exception: string -> theory -> theory; |
31 val allow_abort: string -> theory -> theory; |
32 |
32 |
33 type serialization; |
33 type serialization; |
34 type serializer; |
34 type serializer; |
35 val add_serializer: string * serializer -> theory -> theory; |
35 val add_target: string * serializer -> theory -> theory; |
36 val assert_serializer: theory -> string -> string; |
36 val assert_target: theory -> string -> string; |
37 val serialize: theory -> string -> bool -> string option -> Args.T list |
37 val serialize: theory -> string -> string option -> Args.T list |
38 -> CodeThingol.code -> string list option -> serialization; |
38 -> CodeThingol.program -> string list -> serialization; |
39 val compile: serialization -> unit; |
39 val compile: serialization -> unit; |
40 val write: serialization -> unit; |
40 val write: serialization -> unit; |
41 val file: Path.T -> serialization -> unit; |
41 val file: Path.T -> serialization -> unit; |
42 val string: serialization -> string; |
42 val string: serialization -> string; |
43 val sml_of: theory -> CodeThingol.code -> string list -> string; |
43 |
44 val eval: theory -> (string * (unit -> 'a) option ref) |
44 val code_of: theory -> string -> string -> string list -> string; |
45 -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a; |
45 val eval_conv: string * (unit -> thm) option ref |
46 val target_code_width: int ref; |
46 -> theory -> cterm -> string list -> thm; |
47 val eval_term: string * (unit -> 'a) option ref |
|
48 -> theory -> term -> string list -> 'a; |
|
49 val shell_command: string (*theory name*) -> string (*cg expr*) -> unit; |
|
47 |
50 |
48 val setup: theory -> theory; |
51 val setup: theory -> theory; |
52 val code_width: int ref; |
|
49 end; |
53 end; |
50 |
54 |
51 structure CodeTarget : CODE_TARGET = |
55 structure CodeTarget : CODE_TARGET = |
52 struct |
56 struct |
53 |
57 |
67 | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; |
71 | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; |
68 |
72 |
69 datatype destination = Compile | Write | File of Path.T | String; |
73 datatype destination = Compile | Write | File of Path.T | String; |
70 type serialization = destination -> string option; |
74 type serialization = destination -> string option; |
71 |
75 |
72 val target_code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*) |
76 val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*) |
73 fun target_code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!target_code_width) f); |
77 fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f); |
74 fun target_code_of_pretty p = target_code_setmp Pretty.string_of p ^ "\n"; |
78 fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n"; |
75 fun target_code_writeln p = Pretty.setmp_margin (!target_code_width) Pretty.writeln p; |
79 fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p; |
76 |
80 |
77 (*FIXME why another target_code_setmp?*) |
81 (*FIXME why another code_setmp?*) |
78 fun compile f = (target_code_setmp f Compile; ()); |
82 fun compile f = (code_setmp f Compile; ()); |
79 fun write f = (target_code_setmp f Write; ()); |
83 fun write f = (code_setmp f Write; ()); |
80 fun file p f = (target_code_setmp f (File p); ()); |
84 fun file p f = (code_setmp f (File p); ()); |
81 fun string f = the (target_code_setmp f String); |
85 fun string f = the (code_setmp f String); |
82 |
86 |
83 |
87 |
84 (** generic syntax **) |
88 (** generic syntax **) |
85 |
89 |
86 datatype lrx = L | R | X; |
90 datatype lrx = L | R | X; |
123 -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); |
127 -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); |
124 |
128 |
125 |
129 |
126 (** theory data **) |
130 (** theory data **) |
127 |
131 |
128 val target_diag = "diag"; |
|
129 val target_SML = "SML"; |
132 val target_SML = "SML"; |
130 val target_OCaml = "OCaml"; |
133 val target_OCaml = "OCaml"; |
131 val target_Haskell = "Haskell"; |
134 val target_Haskell = "Haskell"; |
132 |
135 |
133 datatype name_syntax_table = NameSyntaxTable of { |
136 datatype name_syntax_table = NameSyntaxTable of { |
134 class: (string * (string -> string option)) Symtab.table, |
137 class: class_syntax Symtab.table, |
135 inst: unit Symtab.table, |
138 inst: unit Symtab.table, |
136 tyco: typ_syntax Symtab.table, |
139 tyco: typ_syntax Symtab.table, |
137 const: term_syntax Symtab.table |
140 const: term_syntax Symtab.table |
138 }; |
141 }; |
139 |
142 |
158 -> (string * Pretty.T) list (*includes*) |
161 -> (string * Pretty.T) list (*includes*) |
159 -> (string -> string option) (*module aliasses*) |
162 -> (string -> string option) (*module aliasses*) |
160 -> (string -> class_syntax option) |
163 -> (string -> class_syntax option) |
161 -> (string -> typ_syntax option) |
164 -> (string -> typ_syntax option) |
162 -> (string -> term_syntax option) |
165 -> (string -> term_syntax option) |
163 -> CodeThingol.code (*program*) |
166 -> CodeThingol.program |
164 -> string list (*selected statements*) |
167 -> string list (*selected statements*) |
165 -> serialization; |
168 -> serialization; |
166 |
169 |
167 datatype target = Target of { |
170 datatype target = Target of { |
168 serial: serial, |
171 serial: serial, |
207 fun the_reserved (Target { reserved, ... }) = reserved; |
210 fun the_reserved (Target { reserved, ... }) = reserved; |
208 fun the_includes (Target { includes, ... }) = includes; |
211 fun the_includes (Target { includes, ... }) = includes; |
209 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x; |
212 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x; |
210 fun the_module_alias (Target { module_alias , ... }) = module_alias; |
213 fun the_module_alias (Target { module_alias , ... }) = module_alias; |
211 |
214 |
212 fun assert_serializer thy target = |
215 val abort_allowed = snd o CodeTargetData.get; |
216 |
|
217 fun assert_target thy target = |
|
213 case Symtab.lookup (fst (CodeTargetData.get thy)) target |
218 case Symtab.lookup (fst (CodeTargetData.get thy)) target |
214 of SOME data => target |
219 of SOME data => target |
215 | NONE => error ("Unknown code target language: " ^ quote target); |
220 | NONE => error ("Unknown code target language: " ^ quote target); |
216 |
221 |
217 fun add_serializer (target, seri) thy = |
222 fun add_target (target, seri) thy = |
218 let |
223 let |
219 val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target |
224 val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target |
220 of SOME _ => warning ("Overwriting existing serializer " ^ quote target) |
225 of SOME _ => warning ("Overwriting existing serializer " ^ quote target) |
221 | NONE => (); |
226 | NONE => (); |
222 in |
227 in |
226 (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), |
231 (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), |
227 Symtab.empty)))) |
232 Symtab.empty)))) |
228 ((map_target o apfst o apsnd o K) seri) |
233 ((map_target o apfst o apsnd o K) seri) |
229 end; |
234 end; |
230 |
235 |
231 fun map_seri_data target f thy = |
236 fun map_target_data target f thy = |
232 let |
237 let |
233 val _ = assert_serializer thy target; |
238 val _ = assert_target thy target; |
234 in |
239 in |
235 thy |
240 thy |
236 |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f |
241 |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f |
237 end; |
242 end; |
238 |
243 |
239 fun map_adaptions target = |
244 fun map_reserved target = |
240 map_seri_data target o apsnd o apfst; |
245 map_target_data target o apsnd o apfst o apfst; |
246 fun map_includes target = |
|
247 map_target_data target o apsnd o apfst o apsnd; |
|
241 fun map_name_syntax target = |
248 fun map_name_syntax target = |
242 map_seri_data target o apsnd o apsnd o apfst o map_name_syntax_table; |
249 map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table; |
243 fun map_module_alias target = |
250 fun map_module_alias target = |
244 map_seri_data target o apsnd o apsnd o apsnd; |
251 map_target_data target o apsnd o apsnd o apsnd; |
245 |
252 |
246 fun get_serializer get_seri thy target permissive = |
253 fun invoke_serializer thy abortable serializer reserved includes |
247 let |
254 module_alias class inst tyco const module args program1 cs1 = |
248 val (seris, exc) = CodeTargetData.get thy; |
255 let |
249 val data = case Symtab.lookup seris target |
256 val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const; |
257 val cs2 = subtract (op =) hidden cs1; |
|
258 val program2 = Graph.subgraph (not o member (op =) hidden) program1; |
|
259 val all_cs = Graph.all_succs program2 cs2; |
|
260 val program3 = Graph.subgraph (member (op =) all_cs) program2; |
|
261 val empty_funs = filter_out (member (op =) abortable) |
|
262 (CodeThingol.empty_funs program3); |
|
263 val _ = if null empty_funs then () else error ("No defining equations for " |
|
264 ^ commas (map (CodeName.labelled_name thy) empty_funs)); |
|
265 in |
|
266 serializer module args (CodeName.labelled_name thy) reserved includes |
|
267 (Symtab.lookup module_alias) (Symtab.lookup class) |
|
268 (Symtab.lookup tyco) (Symtab.lookup const) |
|
269 program3 cs2 |
|
270 end; |
|
271 |
|
272 fun mount_serializer thy alt_serializer target = |
|
273 let |
|
274 val (targets, abortable) = CodeTargetData.get thy; |
|
275 val data = case Symtab.lookup targets target |
|
250 of SOME data => data |
276 of SOME data => data |
251 | NONE => error ("Unknown code target language: " ^ quote target); |
277 | NONE => error ("Unknown code target language: " ^ quote target); |
252 val seri = get_seri data; |
278 val serializer = the_default (the_serializer data) alt_serializer; |
253 val reserved = the_reserved data; |
279 val reserved = the_reserved data; |
254 val includes = Symtab.dest (the_includes data); |
280 val includes = Symtab.dest (the_includes data); |
255 val alias = the_module_alias data; |
281 val module_alias = the_module_alias data; |
256 val { class, inst, tyco, const } = the_name_syntax data; |
282 val { class, inst, tyco, const } = the_name_syntax data; |
257 val project = if target = target_diag then K I |
283 in |
258 else CodeThingol.project_code permissive |
284 invoke_serializer thy abortable serializer reserved |
259 (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const); |
285 includes module_alias class inst tyco const |
260 fun check_empty_funs code = case filter_out (member (op =) exc) |
|
261 (CodeThingol.empty_funs code) |
|
262 of [] => code |
|
263 | names => error ("No defining equations for " |
|
264 ^ commas (map (CodeName.labelled_name thy) names)); |
|
265 in fn module => fn args => fn code => fn cs => |
|
266 seri module args (CodeName.labelled_name thy) reserved includes |
|
267 (Symtab.lookup alias) (Symtab.lookup class) |
|
268 (Symtab.lookup tyco) (Symtab.lookup const) |
|
269 ((check_empty_funs o project cs) code) (these cs) |
|
270 end; |
286 end; |
271 |
287 |
272 val serialize = get_serializer the_serializer; |
288 fun serialize thy = mount_serializer thy NONE; |
273 |
289 |
274 fun parse_args f args = |
290 fun parse_args f args = |
275 case Scan.read Args.stopper f args |
291 case Scan.read Args.stopper f args |
276 of SOME x => x |
292 of SOME x => x |
277 | NONE => error "Bad serializer arguments"; |
293 | NONE => error "Bad serializer arguments"; |
278 |
294 |
279 |
295 |
280 (** generic output combinators **) |
296 (** generic code combinators **) |
281 |
|
282 (* applications and bindings *) |
|
283 |
|
284 fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons |
|
285 lhs vars fxy (app as ((c, (_, tys)), ts)) = |
|
286 case const_syntax c |
|
287 of NONE => if lhs andalso not (is_cons c) then |
|
288 error ("Non-constructor on left hand side of equation: " ^ labelled_name c) |
|
289 else brackify fxy (pr_app' lhs vars app) |
|
290 | SOME (i, pr) => |
|
291 let |
|
292 val k = if i < 0 then length tys else i; |
|
293 fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys); |
|
294 in if k = length ts |
|
295 then pr' fxy ts |
|
296 else if k < length ts |
|
297 then case chop k ts of (ts1, ts2) => |
|
298 brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2) |
|
299 else pr_term lhs vars fxy (CodeThingol.eta_expand app k) |
|
300 end; |
|
301 |
|
302 fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars = |
|
303 let |
|
304 val vs = case pat |
|
305 of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat [] |
|
306 | NONE => []; |
|
307 val vars' = CodeName.intro_vars (the_list v) vars; |
|
308 val vars'' = CodeName.intro_vars vs vars'; |
|
309 val v' = Option.map (CodeName.lookup_var vars') v; |
|
310 val pat' = Option.map (pr_term true vars'' fxy) pat; |
|
311 in (pr_bind' ((v', pat'), ty), vars'') end; |
|
312 |
|
313 |
297 |
314 (* list, char, string, numeral and monad abstract syntax transformations *) |
298 (* list, char, string, numeral and monad abstract syntax transformations *) |
315 |
299 |
316 fun implode_list c_nil c_cons t = |
300 fun implode_list c_nil c_cons t = |
317 let |
301 let |
357 if negative then SOME ~1 else NONE |
341 if negative then SOME ~1 else NONE |
358 else error "Illegal numeral expression: illegal leading digit" |
342 else error "Illegal numeral expression: illegal leading digit" |
359 | dest_numeral (t1 `$ t2) = |
343 | dest_numeral (t1 `$ t2) = |
360 let val (n, b) = (dest_numeral t2, dest_bit t1) |
344 let val (n, b) = (dest_numeral t2, dest_bit t1) |
361 in case n of SOME n => SOME (2 * n + b) | NONE => NONE end |
345 in case n of SOME n => SOME (2 * n + b) | NONE => NONE end |
362 | dest_numeral _ = error "Illegal numeral expression: illegal constant"; |
346 | dest_numeral _ = error "Illegal numeral expression: illegal term"; |
363 in dest_numeral #> the_default 0 end; |
347 in dest_numeral #> the_default 0 end; |
364 |
348 |
365 fun implode_monad c_bind t = |
349 fun implode_monad c_bind t = |
366 let |
350 let |
367 fun dest_monad (IConst (c, _) `$ t1 `$ t2) = |
351 fun dest_monad (IConst (c, _) `$ t1 `$ t2) = |
376 SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t') |
360 SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t') |
377 | NONE => NONE; |
361 | NONE => NONE; |
378 in CodeThingol.unfoldr dest_monad t end; |
362 in CodeThingol.unfoldr dest_monad t end; |
379 |
363 |
380 |
364 |
365 (* applications and bindings *) |
|
366 |
|
367 fun gen_pr_app pr_app pr_term syntax_const labelled_name is_cons |
|
368 lhs vars fxy (app as ((c, (_, tys)), ts)) = |
|
369 case syntax_const c |
|
370 of NONE => if lhs andalso not (is_cons c) then |
|
371 error ("Non-constructor on left hand side of equation: " ^ labelled_name c) |
|
372 else brackify fxy (pr_app lhs vars app) |
|
373 | SOME (i, pr) => |
|
374 let |
|
375 val k = if i < 0 then length tys else i; |
|
376 fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys); |
|
377 in if k = length ts |
|
378 then pr' fxy ts |
|
379 else if k < length ts |
|
380 then case chop k ts of (ts1, ts2) => |
|
381 brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2) |
|
382 else pr_term lhs vars fxy (CodeThingol.eta_expand app k) |
|
383 end; |
|
384 |
|
385 fun gen_pr_bind pr_bind pr_term (fxy : fixity) ((v, pat), ty : itype) vars = |
|
386 let |
|
387 val vs = case pat |
|
388 of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat [] |
|
389 | NONE => []; |
|
390 val vars' = CodeName.intro_vars (the_list v) vars; |
|
391 val vars'' = CodeName.intro_vars vs vars'; |
|
392 val v' = Option.map (CodeName.lookup_var vars') v; |
|
393 val pat' = Option.map (pr_term true vars'' fxy) pat; |
|
394 in (pr_bind ((v', pat'), ty), vars'') end; |
|
395 |
|
396 |
|
381 (* name auxiliary *) |
397 (* name auxiliary *) |
382 |
398 |
383 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; |
399 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; |
384 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; |
400 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; |
385 |
401 |
386 val dest_name = |
402 val dest_name = |
387 apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode; |
403 apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode; |
388 |
404 |
389 fun mk_modl_name_tab init_names prefix module_alias code = |
405 fun mk_name_module reserved_names module_prefix module_alias program = |
390 let |
406 let |
391 fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode; |
407 fun mk_alias name = case module_alias name |
392 fun mk_alias name = |
408 of SOME name' => name' |
393 case module_alias name |
409 | NONE => name |
394 of SOME name' => name' |
410 |> NameSpace.explode |
395 | NONE => nsp_map (fn name => (the_single o fst) |
411 |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) |
396 (Name.variants [name] init_names)) name; |
412 |> NameSpace.implode; |
397 fun mk_prefix name = |
413 fun mk_prefix name = case module_prefix |
398 case prefix |
414 of SOME module_prefix => NameSpace.append module_prefix name |
399 of SOME prefix => NameSpace.append prefix name |
415 | NONE => name; |
400 | NONE => name; |
|
401 val tab = |
416 val tab = |
402 Symtab.empty |
417 Symtab.empty |
403 |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) |
418 |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) |
404 o fst o dest_name o fst) |
419 o fst o dest_name o fst) |
405 code |
420 program |
406 in fn name => (the o Symtab.lookup tab) name end; |
421 in the o Symtab.lookup tab end; |
407 |
422 |
408 |
423 |
409 |
424 |
410 (** SML/OCaml serializer **) |
425 (** SML/OCaml serializer **) |
411 |
426 |
412 datatype ml_def = |
427 datatype ml_stmt = |
413 MLFuns of (string * (typscheme * (iterm list * iterm) list)) list |
428 MLFuns of (string * (typscheme * (iterm list * iterm) list)) list |
414 | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list |
429 | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list |
415 | MLClass of string * (vname * ((class * string) list * (string * itype) list)) |
430 | MLClass of string * (vname * ((class * string) list * (string * itype) list)) |
416 | MLClassinst of string * ((class * (string * (vname * sort) list)) |
431 | MLClassinst of string * ((class * (string * (vname * sort) list)) |
417 * ((class * (string * (string * dict list list))) list |
432 * ((class * (string * (string * dict list list))) list |
418 * (string * const) list)); |
433 * (string * const) list)); |
419 |
434 |
420 fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def = |
435 fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons = |
421 let |
436 let |
422 val pr_label_classrel = translate_string (fn "." => "__" | c => c) |
437 val pr_label_classrel = translate_string (fn "." => "__" | c => c) |
423 o NameSpace.qualifier; |
438 o NameSpace.qualifier; |
424 val pr_label_classparam = NameSpace.base o NameSpace.qualifier; |
439 val pr_label_classparam = NameSpace.base o NameSpace.qualifier; |
425 fun pr_dicts fxy ds = |
440 fun pr_dicts fxy ds = |
430 p |
445 p |
431 | pr_proj [p'] p = |
446 | pr_proj [p'] p = |
432 brackets [p', p] |
447 brackets [p', p] |
433 | pr_proj (ps as _ :: _) p = |
448 | pr_proj (ps as _ :: _) p = |
434 brackets [Pretty.enum " o" "(" ")" ps, p]; |
449 brackets [Pretty.enum " o" "(" ")" ps, p]; |
435 fun pr_dictc fxy (DictConst (inst, dss)) = |
450 fun pr_dict fxy (DictConst (inst, dss)) = |
436 brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss) |
451 brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss) |
437 | pr_dictc fxy (DictVar (classrels, v)) = |
452 | pr_dict fxy (DictVar (classrels, v)) = |
438 pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v) |
453 pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v) |
439 in case ds |
454 in case ds |
440 of [] => str "()" |
455 of [] => str "()" |
441 | [d] => pr_dictc fxy d |
456 | [d] => pr_dict fxy d |
442 | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds |
457 | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds |
443 end; |
458 end; |
444 fun pr_tyvars vs = |
459 fun pr_tyvar_dicts vs = |
445 vs |
460 vs |
446 |> map (fn (v, sort) => map_index (fn (i, _) => |
461 |> map (fn (v, sort) => map_index (fn (i, _) => |
447 DictVar ([], (v, (i, length sort)))) sort) |
462 DictVar ([], (v, (i, length sort)))) sort) |
448 |> map (pr_dicts BR); |
463 |> map (pr_dicts BR); |
449 fun pr_tycoexpr fxy (tyco, tys) = |
464 fun pr_tycoexpr fxy (tyco, tys) = |
450 let |
465 let |
451 val tyco' = (str o deresolv) tyco |
466 val tyco' = (str o deresolve) tyco |
452 in case map (pr_typ BR) tys |
467 in case map (pr_typ BR) tys |
453 of [] => tyco' |
468 of [] => tyco' |
454 | [p] => Pretty.block [p, Pretty.brk 1, tyco'] |
469 | [p] => Pretty.block [p, Pretty.brk 1, tyco'] |
455 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] |
470 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] |
456 end |
471 end |
457 and pr_typ fxy (tyco `%% tys) = |
472 and pr_typ fxy (tyco `%% tys) = |
458 (case tyco_syntax tyco |
473 (case syntax_tyco tyco |
459 of NONE => pr_tycoexpr fxy (tyco, tys) |
474 of NONE => pr_tycoexpr fxy (tyco, tys) |
460 | SOME (i, pr) => |
475 | SOME (i, pr) => |
461 if not (i = length tys) |
476 if not (i = length tys) |
462 then error ("Number of argument mismatch in customary serialization: " |
477 then error ("Number of argument mismatch in customary serialization: " |
463 ^ (string_of_int o length) tys ^ " given, " |
478 ^ (string_of_int o length) tys ^ " given, " |
482 #>> (fn p => concat [str "fn", p, str "=>"]); |
497 #>> (fn p => concat [str "fn", p, str "=>"]); |
483 val (ps, vars') = fold_map pr binds vars; |
498 val (ps, vars') = fold_map pr binds vars; |
484 in brackets (ps @ [pr_term lhs vars' NOBR t']) end |
499 in brackets (ps @ [pr_term lhs vars' NOBR t']) end |
485 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = |
500 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = |
486 (case CodeThingol.unfold_const_app t0 |
501 (case CodeThingol.unfold_const_app t0 |
487 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
502 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
488 then pr_case vars fxy cases |
503 then pr_case vars fxy cases |
489 else pr_app lhs vars fxy c_ts |
504 else pr_app lhs vars fxy c_ts |
490 | NONE => pr_case vars fxy cases) |
505 | NONE => pr_case vars fxy cases) |
491 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) = |
506 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) = |
492 if is_cons c then let |
507 if is_cons c then let |
493 val k = length tys |
508 val k = length tys |
494 in if k < 2 then |
509 in if k < 2 then |
495 (str o deresolv) c :: map (pr_term lhs vars BR) ts |
510 (str o deresolve) c :: map (pr_term lhs vars BR) ts |
496 else if k = length ts then |
511 else if k = length ts then |
497 [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)] |
512 [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)] |
498 else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else |
513 else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else |
499 (str o deresolv) c |
514 (str o deresolve) c |
500 :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts |
515 :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts |
501 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax |
516 and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const |
502 labelled_name is_cons lhs vars |
517 labelled_name is_cons lhs vars |
503 and pr_bind' ((NONE, NONE), _) = str "_" |
518 and pr_bind' ((NONE, NONE), _) = str "_" |
504 | pr_bind' ((SOME v, NONE), _) = str v |
519 | pr_bind' ((SOME v, NONE), _) = str v |
505 | pr_bind' ((NONE, SOME p), _) = p |
520 | pr_bind' ((NONE, SOME p), _) = p |
506 | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p] |
521 | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p] |
535 :: pr "of" b |
550 :: pr "of" b |
536 :: map (pr "|") bs |
551 :: map (pr "|") bs |
537 ) |
552 ) |
538 end |
553 end |
539 | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\"" |
554 | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\"" |
540 fun pr_def (MLFuns (funns as (funn :: funns'))) = |
555 fun pr_stmt (MLFuns (funns as (funn :: funns'))) = |
541 let |
556 let |
542 val definer = |
557 val definer = |
543 let |
558 let |
544 fun no_args _ ((ts, _) :: _) = length ts |
559 fun no_args _ ((ts, _) :: _) = length ts |
545 | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty; |
560 | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty; |
551 | chk (_, ((vs, ty), eqs)) (SOME defi) = |
566 | chk (_, ((vs, ty), eqs)) (SOME defi) = |
552 if defi = mk (no_args ty eqs) vs then SOME defi |
567 if defi = mk (no_args ty eqs) vs then SOME defi |
553 else error ("Mixing simultaneous vals and funs not implemented: " |
568 else error ("Mixing simultaneous vals and funs not implemented: " |
554 ^ commas (map (labelled_name o fst) funns)); |
569 ^ commas (map (labelled_name o fst) funns)); |
555 in the (fold chk funns NONE) end; |
570 in the (fold chk funns NONE) end; |
556 fun pr_funn definer (name, ((raw_vs, ty), [])) = |
571 fun pr_funn definer (name, ((vs, ty), [])) = |
557 let |
572 let |
558 val vs = filter_out (null o snd) raw_vs; |
573 val vs_dict = filter_out (null o snd) vs; |
559 val n = length vs + (length o fst o CodeThingol.unfold_fun) ty; |
574 val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty; |
560 val exc_str = |
575 val exc_str = |
561 (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; |
576 (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; |
562 in |
577 in |
563 concat ( |
578 concat ( |
564 str definer |
579 str definer |
565 :: (str o deresolv) name |
580 :: (str o deresolve) name |
566 :: map str (replicate n "_") |
581 :: map str (replicate n "_") |
567 @ str "=" |
582 @ str "=" |
568 :: str "raise" |
583 :: str "raise" |
569 :: str "(Fail" |
584 :: str "(Fail" |
570 :: str exc_str |
585 @@ str (exc_str ^ ")") |
571 @@ str ")" |
|
572 ) |
586 ) |
573 end |
587 end |
574 | pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) = |
588 | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) = |
575 let |
589 let |
576 val vs = filter_out (null o snd) raw_vs; |
590 val vs_dict = filter_out (null o snd) vs; |
577 val shift = if null eqs' then I else |
591 val shift = if null eqs' then I else |
578 map (Pretty.block o single o Pretty.block o single); |
592 map (Pretty.block o single o Pretty.block o single); |
579 fun pr_eq definer (ts, t) = |
593 fun pr_eq definer (ts, t) = |
580 let |
594 let |
581 val consts = map_filter |
595 val consts = map_filter |
582 (fn c => if (is_some o const_syntax) c |
596 (fn c => if (is_some o syntax_const) c |
583 then NONE else (SOME o NameSpace.base o deresolv) c) |
597 then NONE else (SOME o NameSpace.base o deresolve) c) |
584 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
598 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
585 val vars = init_syms |
599 val vars = reserved_names |
586 |> CodeName.intro_vars consts |
600 |> CodeName.intro_vars consts |
587 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
601 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
588 (insert (op =)) ts []); |
602 (insert (op =)) ts []); |
589 in |
603 in |
590 concat ( |
604 concat ( |
591 [str definer, (str o deresolv) name] |
605 [str definer, (str o deresolve) name] |
592 @ (if null ts andalso null vs |
606 @ (if null ts andalso null vs_dict |
593 then [str ":", pr_typ NOBR ty] |
607 then [str ":", pr_typ NOBR ty] |
594 else |
608 else |
595 pr_tyvars vs |
609 pr_tyvar_dicts vs_dict |
596 @ map (pr_term true vars BR) ts) |
610 @ map (pr_term true vars BR) ts) |
597 @ [str "=", pr_term false vars NOBR t] |
611 @ [str "=", pr_term false vars NOBR t] |
598 ) |
612 ) |
599 end |
613 end |
600 in |
614 in |
603 :: map (pr_eq "|") eqs' |
617 :: map (pr_eq "|") eqs' |
604 ) |
618 ) |
605 end; |
619 end; |
606 val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns'); |
620 val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns'); |
607 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end |
621 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end |
608 | pr_def (MLDatas (datas as (data :: datas'))) = |
622 | pr_stmt (MLDatas (datas as (data :: datas'))) = |
609 let |
623 let |
610 fun pr_co (co, []) = |
624 fun pr_co (co, []) = |
611 str (deresolv co) |
625 str (deresolve co) |
612 | pr_co (co, tys) = |
626 | pr_co (co, tys) = |
613 concat [ |
627 concat [ |
614 str (deresolv co), |
628 str (deresolve co), |
615 str "of", |
629 str "of", |
616 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys) |
630 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys) |
617 ]; |
631 ]; |
618 fun pr_data definer (tyco, (vs, [])) = |
632 fun pr_data definer (tyco, (vs, [])) = |
619 concat ( |
633 concat ( |
630 :: separate (str "|") (map pr_co cos) |
644 :: separate (str "|") (map pr_co cos) |
631 ); |
645 ); |
632 val (ps, p) = split_last |
646 val (ps, p) = split_last |
633 (pr_data "datatype" data :: map (pr_data "and") datas'); |
647 (pr_data "datatype" data :: map (pr_data "and") datas'); |
634 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end |
648 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end |
635 | pr_def (MLClass (class, (v, (superclasses, classparams)))) = |
649 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = |
636 let |
650 let |
637 val w = first_upper v ^ "_"; |
651 val w = first_upper v ^ "_"; |
638 fun pr_superclass_field (class, classrel) = |
652 fun pr_superclass_field (class, classrel) = |
639 (concat o map str) [ |
653 (concat o map str) [ |
640 pr_label_classrel classrel, ":", "'" ^ v, deresolv class |
654 pr_label_classrel classrel, ":", "'" ^ v, deresolve class |
641 ]; |
655 ]; |
642 fun pr_classparam_field (classparam, ty) = |
656 fun pr_classparam_field (classparam, ty) = |
643 concat [ |
657 concat [ |
644 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty |
658 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty |
645 ]; |
659 ]; |
646 fun pr_classparam_proj (classparam, _) = |
660 fun pr_classparam_proj (classparam, _) = |
647 semicolon [ |
661 semicolon [ |
648 str "fun", |
662 str "fun", |
649 (str o deresolv) classparam, |
663 (str o deresolve) classparam, |
650 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)], |
664 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)], |
651 str "=", |
665 str "=", |
652 str ("#" ^ pr_label_classparam classparam), |
666 str ("#" ^ pr_label_classparam classparam), |
653 str w |
667 str w |
654 ]; |
668 ]; |
655 fun pr_superclass_proj (_, classrel) = |
669 fun pr_superclass_proj (_, classrel) = |
656 semicolon [ |
670 semicolon [ |
657 str "fun", |
671 str "fun", |
658 (str o deresolv) classrel, |
672 (str o deresolve) classrel, |
659 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)], |
673 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)], |
660 str "=", |
674 str "=", |
661 str ("#" ^ pr_label_classrel classrel), |
675 str ("#" ^ pr_label_classrel classrel), |
662 str w |
676 str w |
663 ]; |
677 ]; |
664 in |
678 in |
665 Pretty.chunks ( |
679 Pretty.chunks ( |
666 concat [ |
680 concat [ |
667 str ("type '" ^ v), |
681 str ("type '" ^ v), |
668 (str o deresolv) class, |
682 (str o deresolve) class, |
669 str "=", |
683 str "=", |
670 Pretty.enum "," "{" "};" ( |
684 Pretty.enum "," "{" "};" ( |
671 map pr_superclass_field superclasses @ map pr_classparam_field classparams |
685 map pr_superclass_field superclasses @ map pr_classparam_field classparams |
672 ) |
686 ) |
673 ] |
687 ] |
674 :: map pr_superclass_proj superclasses |
688 :: map pr_superclass_proj superclasses |
675 @ map pr_classparam_proj classparams |
689 @ map pr_classparam_proj classparams |
676 ) |
690 ) |
677 end |
691 end |
678 | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = |
692 | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = |
679 let |
693 let |
680 fun pr_superclass (_, (classrel, dss)) = |
694 fun pr_superclass (_, (classrel, dss)) = |
681 concat [ |
695 concat [ |
682 (str o pr_label_classrel) classrel, |
696 (str o pr_label_classrel) classrel, |
683 str "=", |
697 str "=", |
685 ]; |
699 ]; |
686 fun pr_classparam (classparam, c_inst) = |
700 fun pr_classparam (classparam, c_inst) = |
687 concat [ |
701 concat [ |
688 (str o pr_label_classparam) classparam, |
702 (str o pr_label_classparam) classparam, |
689 str "=", |
703 str "=", |
690 pr_app false init_syms NOBR (c_inst, []) |
704 pr_app false reserved_names NOBR (c_inst, []) |
691 ]; |
705 ]; |
692 in |
706 in |
693 semicolon ([ |
707 semicolon ([ |
694 str (if null arity then "val" else "fun"), |
708 str (if null arity then "val" else "fun"), |
695 (str o deresolv) inst ] @ |
709 (str o deresolve) inst ] @ |
696 pr_tyvars arity @ [ |
710 pr_tyvar_dicts arity @ [ |
697 str "=", |
711 str "=", |
698 Pretty.enum "," "{" "}" |
712 Pretty.enum "," "{" "}" |
699 (map pr_superclass superarities @ map pr_classparam classparam_insts), |
713 (map pr_superclass superarities @ map pr_classparam classparam_insts), |
700 str ":", |
714 str ":", |
701 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) |
715 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) |
702 ]) |
716 ]) |
703 end; |
717 end; |
704 in pr_def ml_def end; |
718 in pr_stmt end; |
705 |
719 |
706 fun pr_sml_modl name content = |
720 fun pr_sml_module name content = |
707 Pretty.chunks ([ |
721 Pretty.chunks ( |
708 str ("structure " ^ name ^ " = "), |
722 str ("structure " ^ name ^ " = ") |
709 str "struct", |
723 :: str "struct" |
710 str "" |
724 :: str "" |
711 ] @ content @ [ |
725 :: content |
712 str "", |
726 @ str "" |
713 str ("end; (*struct " ^ name ^ "*)") |
727 @@ str ("end; (*struct " ^ name ^ "*)") |
714 ]); |
728 ); |
715 |
729 |
716 fun pr_ocaml tyco_syntax const_syntax labelled_name |
730 fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons = |
717 init_syms deresolv is_cons ml_def = |
|
718 let |
731 let |
719 fun pr_dicts fxy ds = |
732 fun pr_dicts fxy ds = |
720 let |
733 let |
721 fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v |
734 fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v |
722 | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1); |
735 | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1); |
723 fun pr_proj ps p = |
736 fun pr_proj ps p = |
724 fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p |
737 fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p |
725 fun pr_dictc fxy (DictConst (inst, dss)) = |
738 fun pr_dict fxy (DictConst (inst, dss)) = |
726 brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss) |
739 brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss) |
727 | pr_dictc fxy (DictVar (classrels, v)) = |
740 | pr_dict fxy (DictVar (classrels, v)) = |
728 pr_proj (map deresolv classrels) ((str o pr_dictvar) v) |
741 pr_proj (map deresolve classrels) ((str o pr_dictvar) v) |
729 in case ds |
742 in case ds |
730 of [] => str "()" |
743 of [] => str "()" |
731 | [d] => pr_dictc fxy d |
744 | [d] => pr_dict fxy d |
732 | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds |
745 | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds |
733 end; |
746 end; |
734 fun pr_tyvars vs = |
747 fun pr_tyvar_dicts vs = |
735 vs |
748 vs |
736 |> map (fn (v, sort) => map_index (fn (i, _) => |
749 |> map (fn (v, sort) => map_index (fn (i, _) => |
737 DictVar ([], (v, (i, length sort)))) sort) |
750 DictVar ([], (v, (i, length sort)))) sort) |
738 |> map (pr_dicts BR); |
751 |> map (pr_dicts BR); |
739 fun pr_tycoexpr fxy (tyco, tys) = |
752 fun pr_tycoexpr fxy (tyco, tys) = |
740 let |
753 let |
741 val tyco' = (str o deresolv) tyco |
754 val tyco' = (str o deresolve) tyco |
742 in case map (pr_typ BR) tys |
755 in case map (pr_typ BR) tys |
743 of [] => tyco' |
756 of [] => tyco' |
744 | [p] => Pretty.block [p, Pretty.brk 1, tyco'] |
757 | [p] => Pretty.block [p, Pretty.brk 1, tyco'] |
745 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] |
758 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] |
746 end |
759 end |
747 and pr_typ fxy (tyco `%% tys) = |
760 and pr_typ fxy (tyco `%% tys) = |
748 (case tyco_syntax tyco |
761 (case syntax_tyco tyco |
749 of NONE => pr_tycoexpr fxy (tyco, tys) |
762 of NONE => pr_tycoexpr fxy (tyco, tys) |
750 | SOME (i, pr) => |
763 | SOME (i, pr) => |
751 if not (i = length tys) |
764 if not (i = length tys) |
752 then error ("Number of argument mismatch in customary serialization: " |
765 then error ("Number of argument mismatch in customary serialization: " |
753 ^ (string_of_int o length) tys ^ " given, " |
766 ^ (string_of_int o length) tys ^ " given, " |
769 val (binds, t') = CodeThingol.unfold_abs t; |
782 val (binds, t') = CodeThingol.unfold_abs t; |
770 fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty); |
783 fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty); |
771 val (ps, vars') = fold_map pr binds vars; |
784 val (ps, vars') = fold_map pr binds vars; |
772 in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end |
785 in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end |
773 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0 |
786 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0 |
774 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
787 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
775 then pr_case vars fxy cases |
788 then pr_case vars fxy cases |
776 else pr_app lhs vars fxy c_ts |
789 else pr_app lhs vars fxy c_ts |
777 | NONE => pr_case vars fxy cases) |
790 | NONE => pr_case vars fxy cases) |
778 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) = |
791 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) = |
779 if is_cons c then |
792 if is_cons c then |
780 if length tys = length ts |
793 if length tys = length ts |
781 then case ts |
794 then case ts |
782 of [] => [(str o deresolv) c] |
795 of [] => [(str o deresolve) c] |
783 | [t] => [(str o deresolv) c, pr_term lhs vars BR t] |
796 | [t] => [(str o deresolve) c, pr_term lhs vars BR t] |
784 | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" |
797 | _ => [(str o deresolve) c, Pretty.enum "," "(" ")" |
785 (map (pr_term lhs vars NOBR) ts)] |
798 (map (pr_term lhs vars NOBR) ts)] |
786 else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))] |
799 else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))] |
787 else (str o deresolv) c |
800 else (str o deresolve) c |
788 :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts) |
801 :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts) |
789 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax |
802 and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const |
790 labelled_name is_cons lhs vars |
803 labelled_name is_cons lhs vars |
791 and pr_bind' ((NONE, NONE), _) = str "_" |
804 and pr_bind' ((NONE, NONE), _) = str "_" |
792 | pr_bind' ((SOME v, NONE), _) = str v |
805 | pr_bind' ((SOME v, NONE), _) = str v |
793 | pr_bind' ((NONE, SOME p), _) = p |
806 | pr_bind' ((NONE, SOME p), _) = p |
794 | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v] |
807 | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v] |
816 :: pr "with" b |
829 :: pr "with" b |
817 :: map (pr "|") bs |
830 :: map (pr "|") bs |
818 ) |
831 ) |
819 end |
832 end |
820 | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\""; |
833 | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\""; |
821 fun pr_def (MLFuns (funns as funn :: funns')) = |
834 fun fish_params vars eqs = |
822 let |
835 let |
823 fun fish_parm _ (w as SOME _) = w |
836 fun fish_param _ (w as SOME _) = w |
824 | fish_parm (IVar v) NONE = SOME v |
837 | fish_param (IVar v) NONE = SOME v |
825 | fish_parm _ NONE = NONE; |
838 | fish_param _ NONE = NONE; |
826 fun fillup_parm _ (_, SOME v) = v |
839 fun fillup_param _ (_, SOME v) = v |
827 | fillup_parm x (i, NONE) = x ^ string_of_int i; |
840 | fillup_param x (i, NONE) = x ^ string_of_int i; |
828 fun fish_parms vars eqs = |
841 val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE); |
829 let |
842 val x = Name.variant (map_filter I fished1) "x"; |
830 val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE); |
843 val fished2 = map_index (fillup_param x) fished1; |
831 val x = Name.variant (map_filter I fished1) "x"; |
844 val (fished3, _) = Name.variants fished2 Name.context; |
832 val fished2 = map_index (fillup_parm x) fished1; |
845 val vars' = CodeName.intro_vars fished3 vars; |
833 val (fished3, _) = Name.variants fished2 Name.context; |
846 in map (CodeName.lookup_var vars') fished3 end; |
834 val vars' = CodeName.intro_vars fished3 vars; |
847 fun pr_stmt (MLFuns (funns as funn :: funns')) = |
835 in map (CodeName.lookup_var vars') fished3 end; |
848 let |
836 fun pr_eq (ts, t) = |
849 fun pr_eq (ts, t) = |
837 let |
850 let |
838 val consts = map_filter |
851 val consts = map_filter |
839 (fn c => if (is_some o const_syntax) c |
852 (fn c => if (is_some o syntax_const) c |
840 then NONE else (SOME o NameSpace.base o deresolv) c) |
853 then NONE else (SOME o NameSpace.base o deresolve) c) |
841 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
854 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
842 val vars = init_syms |
855 val vars = reserved_names |
843 |> CodeName.intro_vars consts |
856 |> CodeName.intro_vars consts |
844 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
857 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
845 (insert (op =)) ts []); |
858 (insert (op =)) ts []); |
846 in concat [ |
859 in concat [ |
847 (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts), |
860 (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts), |
862 ) |
875 ) |
863 end |
876 end |
864 | pr_eqs _ _ [(ts, t)] = |
877 | pr_eqs _ _ [(ts, t)] = |
865 let |
878 let |
866 val consts = map_filter |
879 val consts = map_filter |
867 (fn c => if (is_some o const_syntax) c |
880 (fn c => if (is_some o syntax_const) c |
868 then NONE else (SOME o NameSpace.base o deresolv) c) |
881 then NONE else (SOME o NameSpace.base o deresolve) c) |
869 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
882 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
870 val vars = init_syms |
883 val vars = reserved_names |
871 |> CodeName.intro_vars consts |
884 |> CodeName.intro_vars consts |
872 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
885 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
873 (insert (op =)) ts []); |
886 (insert (op =)) ts []); |
874 in |
887 in |
875 concat ( |
888 concat ( |
889 o single o pr_eq) eqs' |
902 o single o pr_eq) eqs' |
890 ) |
903 ) |
891 | pr_eqs _ _ (eqs as eq :: eqs') = |
904 | pr_eqs _ _ (eqs as eq :: eqs') = |
892 let |
905 let |
893 val consts = map_filter |
906 val consts = map_filter |
894 (fn c => if (is_some o const_syntax) c |
907 (fn c => if (is_some o syntax_const) c |
895 then NONE else (SOME o NameSpace.base o deresolv) c) |
908 then NONE else (SOME o NameSpace.base o deresolve) c) |
896 ((fold o CodeThingol.fold_constnames) |
909 ((fold o CodeThingol.fold_constnames) |
897 (insert (op =)) (map snd eqs) []); |
910 (insert (op =)) (map snd eqs) []); |
898 val vars = init_syms |
911 val vars = reserved_names |
899 |> CodeName.intro_vars consts; |
912 |> CodeName.intro_vars consts; |
900 val dummy_parms = (map str o fish_parms vars o map fst) eqs; |
913 val dummy_parms = (map str o fish_params vars o map fst) eqs; |
901 in |
914 in |
902 Pretty.block ( |
915 Pretty.block ( |
903 Pretty.breaks dummy_parms |
916 Pretty.breaks dummy_parms |
904 @ Pretty.brk 1 |
917 @ Pretty.brk 1 |
905 :: str "=" |
918 :: str "=" |
916 ) |
929 ) |
917 end; |
930 end; |
918 fun pr_funn definer (name, ((vs, ty), eqs)) = |
931 fun pr_funn definer (name, ((vs, ty), eqs)) = |
919 concat ( |
932 concat ( |
920 str definer |
933 str definer |
921 :: (str o deresolv) name |
934 :: (str o deresolve) name |
922 :: pr_tyvars (filter_out (null o snd) vs) |
935 :: pr_tyvar_dicts (filter_out (null o snd) vs) |
923 @| pr_eqs name ty eqs |
936 @| pr_eqs name ty eqs |
924 ); |
937 ); |
925 val (ps, p) = split_last |
938 val (ps, p) = split_last |
926 (pr_funn "let rec" funn :: map (pr_funn "and") funns'); |
939 (pr_funn "let rec" funn :: map (pr_funn "and") funns'); |
927 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end |
940 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end |
928 | pr_def (MLDatas (datas as (data :: datas'))) = |
941 | pr_stmt (MLDatas (datas as (data :: datas'))) = |
929 let |
942 let |
930 fun pr_co (co, []) = |
943 fun pr_co (co, []) = |
931 str (deresolv co) |
944 str (deresolve co) |
932 | pr_co (co, tys) = |
945 | pr_co (co, tys) = |
933 concat [ |
946 concat [ |
934 str (deresolv co), |
947 str (deresolve co), |
935 str "of", |
948 str "of", |
936 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys) |
949 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys) |
937 ]; |
950 ]; |
938 fun pr_data definer (tyco, (vs, [])) = |
951 fun pr_data definer (tyco, (vs, [])) = |
939 concat ( |
952 concat ( |
950 :: separate (str "|") (map pr_co cos) |
963 :: separate (str "|") (map pr_co cos) |
951 ); |
964 ); |
952 val (ps, p) = split_last |
965 val (ps, p) = split_last |
953 (pr_data "type" data :: map (pr_data "and") datas'); |
966 (pr_data "type" data :: map (pr_data "and") datas'); |
954 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end |
967 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end |
955 | pr_def (MLClass (class, (v, (superclasses, classparams)))) = |
968 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = |
956 let |
969 let |
957 val w = "_" ^ first_upper v; |
970 val w = "_" ^ first_upper v; |
958 fun pr_superclass_field (class, classrel) = |
971 fun pr_superclass_field (class, classrel) = |
959 (concat o map str) [ |
972 (concat o map str) [ |
960 deresolv classrel, ":", "'" ^ v, deresolv class |
973 deresolve classrel, ":", "'" ^ v, deresolve class |
961 ]; |
974 ]; |
962 fun pr_classparam_field (classparam, ty) = |
975 fun pr_classparam_field (classparam, ty) = |
963 concat [ |
976 concat [ |
964 (str o deresolv) classparam, str ":", pr_typ NOBR ty |
977 (str o deresolve) classparam, str ":", pr_typ NOBR ty |
965 ]; |
978 ]; |
966 fun pr_classparam_proj (classparam, _) = |
979 fun pr_classparam_proj (classparam, _) = |
967 concat [ |
980 concat [ |
968 str "let", |
981 str "let", |
969 (str o deresolv) classparam, |
982 (str o deresolve) classparam, |
970 str w, |
983 str w, |
971 str "=", |
984 str "=", |
972 str (w ^ "." ^ deresolv classparam ^ ";;") |
985 str (w ^ "." ^ deresolve classparam ^ ";;") |
973 ]; |
986 ]; |
974 in Pretty.chunks ( |
987 in Pretty.chunks ( |
975 concat [ |
988 concat [ |
976 str ("type '" ^ v), |
989 str ("type '" ^ v), |
977 (str o deresolv) class, |
990 (str o deresolve) class, |
978 str "=", |
991 str "=", |
979 enum_default "();;" ";" "{" "};;" ( |
992 enum_default "();;" ";" "{" "};;" ( |
980 map pr_superclass_field superclasses |
993 map pr_superclass_field superclasses |
981 @ map pr_classparam_field classparams |
994 @ map pr_classparam_field classparams |
982 ) |
995 ) |
983 ] |
996 ] |
984 :: map pr_classparam_proj classparams |
997 :: map pr_classparam_proj classparams |
985 ) end |
998 ) end |
986 | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = |
999 | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = |
987 let |
1000 let |
988 fun pr_superclass (_, (classrel, dss)) = |
1001 fun pr_superclass (_, (classrel, dss)) = |
989 concat [ |
1002 concat [ |
990 (str o deresolv) classrel, |
1003 (str o deresolve) classrel, |
991 str "=", |
1004 str "=", |
992 pr_dicts NOBR [DictConst dss] |
1005 pr_dicts NOBR [DictConst dss] |
993 ]; |
1006 ]; |
994 fun pr_classparam_inst (classparam, c_inst) = |
1007 fun pr_classparam_inst (classparam, c_inst) = |
995 concat [ |
1008 concat [ |
996 (str o deresolv) classparam, |
1009 (str o deresolve) classparam, |
997 str "=", |
1010 str "=", |
998 pr_app false init_syms NOBR (c_inst, []) |
1011 pr_app false reserved_names NOBR (c_inst, []) |
999 ]; |
1012 ]; |
1000 in |
1013 in |
1001 concat ( |
1014 concat ( |
1002 str "let" |
1015 str "let" |
1003 :: (str o deresolv) inst |
1016 :: (str o deresolve) inst |
1004 :: pr_tyvars arity |
1017 :: pr_tyvar_dicts arity |
1005 @ str "=" |
1018 @ str "=" |
1006 @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [ |
1019 @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [ |
1007 enum_default "()" ";" "{" "}" (map pr_superclass superarities |
1020 enum_default "()" ";" "{" "}" (map pr_superclass superarities |
1008 @ map pr_classparam_inst classparam_insts), |
1021 @ map pr_classparam_inst classparam_insts), |
1009 str ":", |
1022 str ":", |
1010 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) |
1023 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) |
1011 ] |
1024 ] |
1012 ) |
1025 ) |
1013 end; |
1026 end; |
1014 in pr_def ml_def end; |
1027 in pr_stmt end; |
1015 |
1028 |
1016 fun pr_ocaml_modl name content = |
1029 fun pr_ocaml_module name content = |
1017 Pretty.chunks ([ |
1030 Pretty.chunks ( |
1018 str ("module " ^ name ^ " = "), |
1031 str ("module " ^ name ^ " = ") |
1019 str "struct", |
1032 :: str "struct" |
1020 str "" |
1033 :: str "" |
1021 ] @ content @ [ |
1034 :: content |
1022 str "", |
1035 @ str "" |
1023 str ("end;; (*struct " ^ name ^ "*)") |
1036 @@ str ("end;; (*struct " ^ name ^ "*)") |
1024 ]); |
1037 ); |
1025 |
1038 |
1026 fun seri_ml internal output_cont pr_def pr_modl module labelled_name reserved_syms includes raw_module_alias |
1039 local |
1027 (_ : string -> class_syntax option) tyco_syntax const_syntax code cs seri_dest = |
1040 |
1028 let |
1041 datatype ml_node = |
1029 val module_alias = if is_some module then K module else raw_module_alias; |
1042 Dummy of string |
1030 val is_cons = CodeThingol.is_cons code; |
1043 | Stmt of string * ml_stmt |
1031 datatype node = |
1044 | Module of string * ((Name.context * Name.context) * ml_node Graph.T); |
1032 Def of string * ml_def option |
1045 |
1033 | Module of string * ((Name.context * Name.context) * node Graph.T); |
1046 in |
1034 val init_names = Name.make_context reserved_syms; |
1047 |
1035 val init_module = ((init_names, init_names), Graph.empty); |
1048 fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program = |
1049 let |
|
1050 val module_alias = if is_some module_name then K module_name else raw_module_alias; |
|
1051 val reserved_names = Name.make_context reserved_names; |
|
1052 val empty_module = ((reserved_names, reserved_names), Graph.empty); |
|
1036 fun map_node [] f = f |
1053 fun map_node [] f = f |
1037 | map_node (m::ms) f = |
1054 | map_node (m::ms) f = |
1038 Graph.default_node (m, Module (m, init_module)) |
1055 Graph.default_node (m, Module (m, empty_module)) |
1039 #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => |
1056 #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) => |
1040 Module (dmodlname, (nsp, map_node ms f nodes))); |
1057 Module (module_name, (nsp, map_node ms f nodes))); |
1041 fun map_nsp_yield [] f (nsp, nodes) = |
1058 fun map_nsp_yield [] f (nsp, nodes) = |
1042 let |
1059 let |
1043 val (x, nsp') = f nsp |
1060 val (x, nsp') = f nsp |
1044 in (x, (nsp', nodes)) end |
1061 in (x, (nsp', nodes)) end |
1045 | map_nsp_yield (m::ms) f (nsp, nodes) = |
1062 | map_nsp_yield (m::ms) f (nsp, nodes) = |
1046 let |
1063 let |
1047 val (x, nodes') = |
1064 val (x, nodes') = |
1048 nodes |
1065 nodes |
1049 |> Graph.default_node (m, Module (m, init_module)) |
1066 |> Graph.default_node (m, Module (m, empty_module)) |
1050 |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) => |
1067 |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => |
1051 let |
1068 let |
1052 val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes |
1069 val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes |
1053 in (x, Module (dmodlname, nsp_nodes')) end) |
1070 in (x, Module (d_module_name, nsp_nodes')) end) |
1054 in (x, (nsp, nodes')) end; |
1071 in (x, (nsp, nodes')) end; |
1055 val init_syms = CodeName.make_vars reserved_syms; |
1072 fun map_nsp_fun_yield f (nsp_fun, nsp_typ) = |
1056 val name_modl = mk_modl_name_tab init_names NONE module_alias code; |
1073 let |
1057 fun name_def upper name nsp = |
1074 val (x, nsp_fun') = f nsp_fun |
1075 in (x, (nsp_fun', nsp_typ)) end; |
|
1076 fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = |
|
1077 let |
|
1078 val (x, nsp_typ') = f nsp_typ |
|
1079 in (x, (nsp_fun, nsp_typ')) end; |
|
1080 val mk_name_module = mk_name_module reserved_names NONE module_alias program; |
|
1081 fun mk_name_stmt upper name nsp = |
|
1058 let |
1082 let |
1059 val (_, base) = dest_name name; |
1083 val (_, base) = dest_name name; |
1060 val base' = if upper then first_upper base else base; |
1084 val base' = if upper then first_upper base else base; |
1061 val ([base''], nsp') = Name.variants [base'] nsp; |
1085 val ([base''], nsp') = Name.variants [base'] nsp; |
1062 in (base'', nsp') end; |
1086 in (base'', nsp') end; |
1063 fun map_nsp_fun f (nsp_fun, nsp_typ) = |
1087 fun add_funs stmts = |
1064 let |
|
1065 val (x, nsp_fun') = f nsp_fun |
|
1066 in (x, (nsp_fun', nsp_typ)) end; |
|
1067 fun map_nsp_typ f (nsp_fun, nsp_typ) = |
|
1068 let |
|
1069 val (x, nsp_typ') = f nsp_typ |
|
1070 in (x, (nsp_fun, nsp_typ')) end; |
|
1071 fun mk_funs defs = |
|
1072 fold_map |
1088 fold_map |
1073 (fn (name, CodeThingol.Fun info) => |
1089 (fn (name, CodeThingol.Fun stmt) => |
1074 map_nsp_fun (name_def false name) >> |
1090 map_nsp_fun_yield (mk_name_stmt false name) #>> |
1075 (fn base => (base, (name, (apsnd o map) fst info))) |
1091 rpair (name, (apsnd o map) fst stmt) |
1076 | (name, def) => |
1092 | (name, _) => |
1077 error ("Function block containing illegal statement: " ^ labelled_name name) |
1093 error ("Function block containing illegal statement: " ^ labelled_name name) |
1078 ) defs |
1094 ) stmts |
1079 >> (split_list #> apsnd MLFuns); |
1095 #>> (split_list #> apsnd MLFuns); |
1080 fun mk_datatype defs = |
1096 fun add_datatypes stmts = |
1081 fold_map |
1097 fold_map |
1082 (fn (name, CodeThingol.Datatype info) => |
1098 (fn (name, CodeThingol.Datatype stmt) => |
1083 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info))) |
1099 map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) |
1084 | (name, CodeThingol.Datatypecons _) => |
1100 | (name, CodeThingol.Datatypecons _) => |
1085 map_nsp_fun (name_def true name) >> (fn base => (base, NONE)) |
1101 map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE |
1086 | (name, def) => |
1102 | (name, _) => |
1087 error ("Datatype block containing illegal statement: " ^ labelled_name name) |
1103 error ("Datatype block containing illegal statement: " ^ labelled_name name) |
1088 ) defs |
1104 ) stmts |
1089 >> (split_list #> apsnd (map_filter I |
1105 #>> (split_list #> apsnd (map_filter I |
1090 #> (fn [] => error ("Datatype block without data statement: " |
1106 #> (fn [] => error ("Datatype block without data statement: " |
1091 ^ (commas o map (labelled_name o fst)) defs) |
1107 ^ (commas o map (labelled_name o fst)) stmts) |
1092 | infos => MLDatas infos))); |
1108 | stmts => MLDatas stmts))); |
1093 fun mk_class defs = |
1109 fun add_class stmts = |
1094 fold_map |
1110 fold_map |
1095 (fn (name, CodeThingol.Class info) => |
1111 (fn (name, CodeThingol.Class info) => |
1096 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info))) |
1112 map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info)) |
1097 | (name, CodeThingol.Classrel _) => |
1113 | (name, CodeThingol.Classrel _) => |
1098 map_nsp_fun (name_def false name) >> (fn base => (base, NONE)) |
1114 map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE |
1099 | (name, CodeThingol.Classparam _) => |
1115 | (name, CodeThingol.Classparam _) => |
1100 map_nsp_fun (name_def false name) >> (fn base => (base, NONE)) |
1116 map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE |
1101 | (name, def) => |
1117 | (name, _) => |
1102 error ("Class block containing illegal statement: " ^ labelled_name name) |
1118 error ("Class block containing illegal statement: " ^ labelled_name name) |
1103 ) defs |
1119 ) stmts |
1104 >> (split_list #> apsnd (map_filter I |
1120 #>> (split_list #> apsnd (map_filter I |
1105 #> (fn [] => error ("Class block without class statement: " |
1121 #> (fn [] => error ("Class block without class statement: " |
1106 ^ (commas o map (labelled_name o fst)) defs) |
1122 ^ (commas o map (labelled_name o fst)) stmts) |
1107 | [info] => MLClass info))); |
1123 | [stmt] => MLClass stmt))); |
1108 fun mk_inst [(name, CodeThingol.Classinst info)] = |
1124 fun add_inst [(name, CodeThingol.Classinst stmt)] = |
1109 map_nsp_fun (name_def false name) |
1125 map_nsp_fun_yield (mk_name_stmt false name) |
1110 >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info))); |
1126 #>> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst stmt))); |
1111 fun add_group mk defs nsp_nodes = |
1127 fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) = |
1128 add_funs stmts |
|
1129 | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) = |
|
1130 add_datatypes stmts |
|
1131 | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) = |
|
1132 add_datatypes stmts |
|
1133 | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) = |
|
1134 add_class stmts |
|
1135 | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) = |
|
1136 add_class stmts |
|
1137 | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) = |
|
1138 add_class stmts |
|
1139 | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) = |
|
1140 add_inst stmts |
|
1141 | add_stmts stmts = error ("Illegal mutual dependencies: " ^ |
|
1142 (commas o map (labelled_name o fst)) stmts); |
|
1143 fun add_stmts' stmts nsp_nodes = |
|
1112 let |
1144 let |
1113 val names as (name :: names') = map fst defs; |
1145 val names as (name :: names') = map fst stmts; |
1114 val deps = |
1146 val deps = |
1115 [] |
1147 [] |
1116 |> fold (fold (insert (op =)) o Graph.imm_succs code) names |
1148 |> fold (fold (insert (op =)) o Graph.imm_succs program) names |
1117 |> subtract (op =) names; |
1149 |> subtract (op =) names; |
1118 val (modls, _) = (split_list o map dest_name) names; |
1150 val (module_names, _) = (split_list o map dest_name) names; |
1119 val modl' = (the_single o distinct (op =) o map name_modl) modls |
1151 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names |
1120 handle Empty => |
1152 handle Empty => |
1121 error ("Different namespace prefixes for mutual dependencies:\n" |
1153 error ("Different namespace prefixes for mutual dependencies:\n" |
1122 ^ commas (map labelled_name names) |
1154 ^ commas (map labelled_name names) |
1123 ^ "\n" |
1155 ^ "\n" |
1124 ^ commas (map (NameSpace.qualifier o NameSpace.qualifier) names)); |
1156 ^ commas module_names); |
1125 val modl_explode = NameSpace.explode modl'; |
1157 val module_name_path = NameSpace.explode module_name; |
1126 fun add_dep name name'' = |
1158 fun add_dep name name' = |
1127 let |
1159 let |
1128 val modl'' = (name_modl o fst o dest_name) name''; |
1160 val module_name' = (mk_name_module o fst o dest_name) name'; |
1129 in if modl' = modl'' then |
1161 in if module_name = module_name' then |
1130 map_node modl_explode |
1162 map_node module_name_path (Graph.add_edge (name, name')) |
1131 (Graph.add_edge (name, name'')) |
|
1132 else let |
1163 else let |
1133 val (common, (diff1::_, diff2::_)) = chop_prefix (op =) |
1164 val (common, (diff1::_, diff2::_)) = chop_prefix (op =) |
1134 (modl_explode, NameSpace.explode modl''); |
1165 (module_name_path, NameSpace.explode module_name'); |
1135 in |
1166 in |
1136 map_node common |
1167 map_node common |
1137 (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr |
1168 (fn node => Graph.add_edge_acyclic (diff1, diff2) node |
1138 handle Graph.CYCLES _ => error ("Dependency " |
1169 handle Graph.CYCLES _ => error ("Dependency " |
1139 ^ quote name ^ " -> " ^ quote name'' |
1170 ^ quote name ^ " -> " ^ quote name' |
1140 ^ " would result in module dependency cycle")) |
1171 ^ " would result in module dependency cycle")) |
1141 end end; |
1172 end end; |
1142 in |
1173 in |
1143 nsp_nodes |
1174 nsp_nodes |
1144 |> map_nsp_yield modl_explode (mk defs) |
1175 |> map_nsp_yield module_name_path (add_stmts stmts) |
1145 |-> (fn (base' :: bases', def') => |
1176 |-> (fn (base' :: bases', stmt') => |
1146 apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def'))) |
1177 apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt'))) |
1147 #> fold2 (fn name' => fn base' => |
1178 #> fold2 (fn name' => fn base' => |
1148 Graph.new_node (name', (Def (base', NONE)))) names' bases'))) |
1179 Graph.new_node (name', (Dummy base'))) names' bases'))) |
1149 |> apsnd (fold (fn name => fold (add_dep name) deps) names) |
1180 |> apsnd (fold (fn name => fold (add_dep name) deps) names) |
1150 |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names) |
1181 |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names) |
1151 end; |
1182 end; |
1152 fun group_defs ((defs as (_, CodeThingol.Fun _)::_)) = |
1183 val (_, nodes) = empty_module |
1153 add_group mk_funs defs |
1184 |> fold add_stmts' (map (AList.make (Graph.get_node program)) |
1154 | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) = |
1185 (rev (Graph.strong_conn program))); |
1155 add_group mk_datatype defs |
|
1156 | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) = |
|
1157 add_group mk_datatype defs |
|
1158 | group_defs ((defs as (_, CodeThingol.Class _)::_)) = |
|
1159 add_group mk_class defs |
|
1160 | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) = |
|
1161 add_group mk_class defs |
|
1162 | group_defs ((defs as (_, CodeThingol.Classparam _)::_)) = |
|
1163 add_group mk_class defs |
|
1164 | group_defs ((defs as [(_, CodeThingol.Classinst _)])) = |
|
1165 add_group mk_inst defs |
|
1166 | group_defs defs = error ("Illegal mutual dependencies: " ^ |
|
1167 (commas o map (labelled_name o fst)) defs) |
|
1168 val (_, nodes) = |
|
1169 init_module |
|
1170 |> fold group_defs (map (AList.make (Graph.get_node code)) |
|
1171 (rev (Graph.strong_conn code))) |
|
1172 fun deresolver prefix name = |
1186 fun deresolver prefix name = |
1173 let |
1187 let |
1174 val modl = (fst o dest_name) name; |
1188 val module_name = (fst o dest_name) name; |
1175 val modl' = (NameSpace.explode o name_modl) modl; |
1189 val module_name' = (NameSpace.explode o mk_name_module) module_name; |
1176 val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl'); |
1190 val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); |
1177 val defname' = |
1191 val stmt_name = |
1178 nodes |
1192 nodes |
1179 |> fold (fn m => fn g => case Graph.get_node g m |
1193 |> fold (fn name => fn node => case Graph.get_node node name |
1180 of Module (_, (_, g)) => g) modl' |
1194 of Module (_, (_, node)) => node) module_name' |
1181 |> (fn g => case Graph.get_node g name of Def (defname, _) => defname); |
1195 |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name |
1196 | Dummy stmt_name => stmt_name); |
|
1182 in |
1197 in |
1183 NameSpace.implode (remainder @ [defname']) |
1198 NameSpace.implode (remainder @ [stmt_name]) |
1184 end handle Graph.UNDEF _ => |
1199 end handle Graph.UNDEF _ => |
1185 error ("Unknown statement name: " ^ labelled_name name); |
1200 error ("Unknown statement name: " ^ labelled_name name); |
1186 fun pr_node prefix (Def (_, NONE)) = |
1201 in (deresolver, nodes) end; |
1202 |
|
1203 fun serialize_ml compile pr_module pr_stmt projection module_name labelled_name reserved_names includes raw_module_alias |
|
1204 _ syntax_tyco syntax_const program cs destination = |
|
1205 let |
|
1206 val is_cons = CodeThingol.is_cons program; |
|
1207 val (deresolver, nodes) = ml_node_of_program labelled_name module_name |
|
1208 reserved_names raw_module_alias program; |
|
1209 val reserved_names = CodeName.make_vars reserved_names; |
|
1210 fun pr_node prefix (Dummy _) = |
|
1187 NONE |
1211 NONE |
1188 | pr_node prefix (Def (_, SOME def)) = |
1212 | pr_node prefix (Stmt (_, def)) = |
1189 SOME (pr_def tyco_syntax const_syntax labelled_name init_syms |
1213 SOME (pr_stmt syntax_tyco syntax_const labelled_name reserved_names |
1190 (deresolver prefix) is_cons def) |
1214 (deresolver prefix) is_cons def) |
1191 | pr_node prefix (Module (dmodlname, (_, nodes))) = |
1215 | pr_node prefix (Module (module_name, (_, nodes))) = |
1192 SOME (pr_modl dmodlname ( |
1216 SOME (pr_module module_name ( |
1193 separate (str "") |
1217 separate (str "") |
1194 ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes) |
1218 ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes) |
1195 o rev o flat o Graph.strong_conn) nodes))); |
1219 o rev o flat o Graph.strong_conn) nodes))); |
1220 val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else []))) |
|
1221 cs; |
|
1196 val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter |
1222 val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter |
1197 (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)); |
1223 (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)); |
1198 val deresolv = try (deresolver (if is_some module then the_list module else [])); |
1224 fun output Compile = K NONE o compile o code_of_pretty |
1199 val output = case seri_dest |
1225 | output Write = K NONE o code_writeln |
1200 of Compile => K NONE o internal o target_code_of_pretty |
1226 | output (File file) = K NONE o File.write file o code_of_pretty |
1201 | Write => K NONE o target_code_writeln |
1227 | output String = SOME o code_of_pretty; |
1202 | File file => K NONE o File.write file o target_code_of_pretty |
1228 in projection (output destination p) cs' end; |
1203 | String => SOME o target_code_of_pretty; |
1229 |
1204 in output_cont (map_filter deresolv cs, output p) end; |
1230 end; (*local*) |
1205 |
1231 |
1206 fun isar_seri_sml module = |
1232 fun isar_seri_sml module_name = |
1207 parse_args (Scan.succeed ()) |
1233 parse_args (Scan.succeed ()) |
1208 #> (fn () => seri_ml (use_text (1, "generated code") Output.ml_output false) snd pr_sml pr_sml_modl module); |
1234 #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false) |
1209 |
1235 pr_sml_module pr_sml_stmt K module_name); |
1210 fun isar_seri_ocaml module = |
1236 |
1237 fun isar_seri_ocaml module_name = |
|
1211 parse_args (Scan.succeed ()) |
1238 parse_args (Scan.succeed ()) |
1212 #> (fn () => seri_ml (fn _ => error "OCaml: no internal compilation") snd pr_ocaml pr_ocaml_modl module) |
1239 #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation") |
1240 pr_ocaml_module pr_ocaml_stmt K module_name); |
|
1213 |
1241 |
1214 |
1242 |
1215 (** Haskell serializer **) |
1243 (** Haskell serializer **) |
1216 |
1244 |
1217 local |
1245 val pr_haskell_bind = |
1218 |
1246 let |
1219 fun pr_bind' ((NONE, NONE), _) = str "_" |
1247 fun pr_bind ((NONE, NONE), _) = str "_" |
1220 | pr_bind' ((SOME v, NONE), _) = str v |
1248 | pr_bind ((SOME v, NONE), _) = str v |
1221 | pr_bind' ((NONE, SOME p), _) = p |
1249 | pr_bind ((NONE, SOME p), _) = p |
1222 | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p] |
1250 | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p]; |
1223 |
1251 in gen_pr_bind pr_bind end; |
1224 val pr_bind_haskell = gen_pr_bind pr_bind'; |
1252 |
1225 |
1253 fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name |
1226 in |
1254 init_syms deresolve is_cons contr_classparam_typs deriving_show = |
1227 |
1255 let |
1228 fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name |
1256 val deresolve_base = NameSpace.base o deresolve; |
1229 init_syms deresolv_here deresolv is_cons contr_classparam_typs deriving_show def = |
1257 fun class_name class = case syntax_class class |
1230 let |
1258 of NONE => deresolve class |
1231 fun class_name class = case class_syntax class |
|
1232 of NONE => deresolv class |
|
1233 | SOME (class, _) => class; |
1259 | SOME (class, _) => class; |
1234 fun classparam_name class classparam = case class_syntax class |
1260 fun classparam_name class classparam = case syntax_class class |
1235 of NONE => deresolv_here classparam |
1261 of NONE => deresolve_base classparam |
1236 | SOME (_, classparam_syntax) => case classparam_syntax classparam |
1262 | SOME (_, classparam_syntax) => case classparam_syntax classparam |
1237 of NONE => (snd o dest_name) classparam |
1263 of NONE => (snd o dest_name) classparam |
1238 | SOME classparam => classparam; |
1264 | SOME classparam => classparam; |
1239 fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs |
1265 fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs |
1240 of [] => [] |
1266 of [] => [] |
1247 | vnames => str "forall " :: Pretty.breaks |
1273 | vnames => str "forall " :: Pretty.breaks |
1248 (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; |
1274 (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; |
1249 fun pr_tycoexpr tyvars fxy (tyco, tys) = |
1275 fun pr_tycoexpr tyvars fxy (tyco, tys) = |
1250 brackify fxy (str tyco :: map (pr_typ tyvars BR) tys) |
1276 brackify fxy (str tyco :: map (pr_typ tyvars BR) tys) |
1251 and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = |
1277 and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = |
1252 (case tyco_syntax tyco |
1278 (case syntax_tyco tyco |
1253 of NONE => |
1279 of NONE => |
1254 pr_tycoexpr tyvars fxy (deresolv tyco, tys) |
1280 pr_tycoexpr tyvars fxy (deresolve tyco, tys) |
1255 | SOME (i, pr) => |
1281 | SOME (i, pr) => |
1256 if not (i = length tys) |
1282 if not (i = length tys) |
1257 then error ("Number of argument mismatch in customary serialization: " |
1283 then error ("Number of argument mismatch in customary serialization: " |
1258 ^ (string_of_int o length) tys ^ " given, " |
1284 ^ (string_of_int o length) tys ^ " given, " |
1259 ^ string_of_int i ^ " expected") |
1285 ^ string_of_int i ^ " expected") |
1282 fun pr ((v, pat), ty) = pr_bind tyvars BR ((SOME v, pat), ty); |
1308 fun pr ((v, pat), ty) = pr_bind tyvars BR ((SOME v, pat), ty); |
1283 val (ps, vars') = fold_map pr binds vars; |
1309 val (ps, vars') = fold_map pr binds vars; |
1284 in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end |
1310 in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end |
1285 | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) = |
1311 | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) = |
1286 (case CodeThingol.unfold_const_app t0 |
1312 (case CodeThingol.unfold_const_app t0 |
1287 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
1313 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
1288 then pr_case tyvars vars fxy cases |
1314 then pr_case tyvars vars fxy cases |
1289 else pr_app tyvars lhs vars fxy c_ts |
1315 else pr_app tyvars lhs vars fxy c_ts |
1290 | NONE => pr_case tyvars vars fxy cases) |
1316 | NONE => pr_case tyvars vars fxy cases) |
1291 and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c |
1317 and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c |
1292 of [] => (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts |
1318 of [] => (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts |
1293 | fingerprint => let |
1319 | fingerprint => let |
1294 val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint; |
1320 val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint; |
1295 val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) => |
1321 val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) => |
1296 (not o CodeThingol.locally_monomorphic) t) ts_fingerprint; |
1322 (not o CodeThingol.locally_monomorphic) t) ts_fingerprint; |
1297 fun pr_term_anno (t, NONE) _ = pr_term tyvars lhs vars BR t |
1323 fun pr_term_anno (t, NONE) _ = pr_term tyvars lhs vars BR t |
1298 | pr_term_anno (t, SOME _) ty = |
1324 | pr_term_anno (t, SOME _) ty = |
1299 brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty]; |
1325 brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty]; |
1300 in |
1326 in |
1301 if needs_annotation then |
1327 if needs_annotation then |
1302 (str o deresolv) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys) |
1328 (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys) |
1303 else (str o deresolv) c :: map (pr_term tyvars lhs vars BR) ts |
1329 else (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts |
1304 end |
1330 end |
1305 and pr_app tyvars lhs vars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) const_syntax |
1331 and pr_app tyvars lhs vars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const |
1306 labelled_name is_cons lhs vars |
1332 labelled_name is_cons lhs vars |
1307 and pr_bind tyvars = pr_bind_haskell (pr_term tyvars) |
1333 and pr_bind tyvars = pr_haskell_bind (pr_term tyvars) |
1308 and pr_case tyvars vars fxy (cases as ((_, [_]), _)) = |
1334 and pr_case tyvars vars fxy (cases as ((_, [_]), _)) = |
1309 let |
1335 let |
1310 val (binds, t) = CodeThingol.unfold_let (ICase cases); |
1336 val (binds, t) = CodeThingol.unfold_let (ICase cases); |
1311 fun pr ((pat, ty), t) vars = |
1337 fun pr ((pat, ty), t) vars = |
1312 vars |
1338 vars |
1330 concat [str "(case", pr_term tyvars false vars NOBR td, str "of", str "{"], |
1356 concat [str "(case", pr_term tyvars false vars NOBR td, str "of", str "{"], |
1331 str "})" |
1357 str "})" |
1332 ) (map pr bs) |
1358 ) (map pr bs) |
1333 end |
1359 end |
1334 | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\""; |
1360 | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\""; |
1335 fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) = |
1361 fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) = |
1336 let |
1362 let |
1337 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1363 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1338 val n = (length o fst o CodeThingol.unfold_fun) ty; |
1364 val n = (length o fst o CodeThingol.unfold_fun) ty; |
1339 in |
1365 in |
1340 Pretty.chunks [ |
1366 Pretty.chunks [ |
1341 Pretty.block [ |
1367 Pretty.block [ |
1342 (str o suffix " ::" o deresolv_here) name, |
1368 (str o suffix " ::" o deresolve_base) name, |
1343 Pretty.brk 1, |
1369 Pretty.brk 1, |
1344 pr_typscheme tyvars (vs, ty), |
1370 pr_typscheme tyvars (vs, ty), |
1345 str ";" |
1371 str ";" |
1346 ], |
1372 ], |
1347 concat ( |
1373 concat ( |
1348 (str o deresolv_here) name |
1374 (str o deresolve_base) name |
1349 :: map str (replicate n "_") |
1375 :: map str (replicate n "_") |
1350 @ str "=" |
1376 @ str "=" |
1351 :: str "error" |
1377 :: str "error" |
1352 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string |
1378 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string |
1353 o NameSpace.base o NameSpace.qualifier) name |
1379 o NameSpace.base o NameSpace.qualifier) name |
1354 ) |
1380 ) |
1355 ] |
1381 ] |
1356 end |
1382 end |
1357 | pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) = |
1383 | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) = |
1358 let |
1384 let |
1359 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1385 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1360 fun pr_eq ((ts, t), _) = |
1386 fun pr_eq ((ts, t), _) = |
1361 let |
1387 let |
1362 val consts = map_filter |
1388 val consts = map_filter |
1363 (fn c => if (is_some o const_syntax) c |
1389 (fn c => if (is_some o syntax_const) c |
1364 then NONE else (SOME o NameSpace.base o deresolv) c) |
1390 then NONE else (SOME o NameSpace.base o deresolve) c) |
1365 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
1391 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []); |
1366 val vars = init_syms |
1392 val vars = init_syms |
1367 |> CodeName.intro_vars consts |
1393 |> CodeName.intro_vars consts |
1368 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
1394 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames) |
1369 (insert (op =)) ts []); |
1395 (insert (op =)) ts []); |
1370 in |
1396 in |
1371 semicolon ( |
1397 semicolon ( |
1372 (str o deresolv_here) name |
1398 (str o deresolve_base) name |
1373 :: map (pr_term tyvars true vars BR) ts |
1399 :: map (pr_term tyvars true vars BR) ts |
1374 @ str "=" |
1400 @ str "=" |
1375 @@ pr_term tyvars false vars NOBR t |
1401 @@ pr_term tyvars false vars NOBR t |
1376 ) |
1402 ) |
1377 end; |
1403 end; |
1378 in |
1404 in |
1379 Pretty.chunks ( |
1405 Pretty.chunks ( |
1380 Pretty.block [ |
1406 Pretty.block [ |
1381 (str o suffix " ::" o deresolv_here) name, |
1407 (str o suffix " ::" o deresolve_base) name, |
1382 Pretty.brk 1, |
1408 Pretty.brk 1, |
1383 pr_typscheme tyvars (vs, ty), |
1409 pr_typscheme tyvars (vs, ty), |
1384 str ";" |
1410 str ";" |
1385 ] |
1411 ] |
1386 :: map pr_eq eqs |
1412 :: map pr_eq eqs |
1387 ) |
1413 ) |
1388 end |
1414 end |
1389 | pr_def (name, CodeThingol.Datatype (vs, [])) = |
1415 | pr_stmt (name, CodeThingol.Datatype (vs, [])) = |
1390 let |
1416 let |
1391 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1417 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1392 in |
1418 in |
1393 semicolon [ |
1419 semicolon [ |
1394 str "data", |
1420 str "data", |
1395 pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs)) |
1421 pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) |
1396 ] |
1422 ] |
1397 end |
1423 end |
1398 | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) = |
1424 | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) = |
1399 let |
1425 let |
1400 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1426 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1401 in |
1427 in |
1402 semicolon ( |
1428 semicolon ( |
1403 str "newtype" |
1429 str "newtype" |
1404 :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs)) |
1430 :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) |
1405 :: str "=" |
1431 :: str "=" |
1406 :: (str o deresolv_here) co |
1432 :: (str o deresolve_base) co |
1407 :: pr_typ tyvars BR ty |
1433 :: pr_typ tyvars BR ty |
1408 :: (if deriving_show name then [str "deriving (Read, Show)"] else []) |
1434 :: (if deriving_show name then [str "deriving (Read, Show)"] else []) |
1409 ) |
1435 ) |
1410 end |
1436 end |
1411 | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) = |
1437 | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) = |
1412 let |
1438 let |
1413 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1439 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1414 fun pr_co (co, tys) = |
1440 fun pr_co (co, tys) = |
1415 concat ( |
1441 concat ( |
1416 (str o deresolv_here) co |
1442 (str o deresolve_base) co |
1417 :: map (pr_typ tyvars BR) tys |
1443 :: map (pr_typ tyvars BR) tys |
1418 ) |
1444 ) |
1419 in |
1445 in |
1420 semicolon ( |
1446 semicolon ( |
1421 str "data" |
1447 str "data" |
1422 :: pr_typdecl tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs)) |
1448 :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) |
1423 :: str "=" |
1449 :: str "=" |
1424 :: pr_co co |
1450 :: pr_co co |
1425 :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos |
1451 :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos |
1426 @ (if deriving_show name then [str "deriving (Read, Show)"] else []) |
1452 @ (if deriving_show name then [str "deriving (Read, Show)"] else []) |
1427 ) |
1453 ) |
1428 end |
1454 end |
1429 | pr_def (name, CodeThingol.Class (v, (superclasses, classparams))) = |
1455 | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) = |
1430 let |
1456 let |
1431 val tyvars = CodeName.intro_vars [v] init_syms; |
1457 val tyvars = CodeName.intro_vars [v] init_syms; |
1432 fun pr_classparam (classparam, ty) = |
1458 fun pr_classparam (classparam, ty) = |
1433 semicolon [ |
1459 semicolon [ |
1434 (str o classparam_name name) classparam, |
1460 (str o classparam_name name) classparam, |
1438 in |
1464 in |
1439 Pretty.block_enclose ( |
1465 Pretty.block_enclose ( |
1440 Pretty.block [ |
1466 Pretty.block [ |
1441 str "class ", |
1467 str "class ", |
1442 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]), |
1468 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]), |
1443 str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v), |
1469 str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v), |
1444 str " where {" |
1470 str " where {" |
1445 ], |
1471 ], |
1446 str "};" |
1472 str "};" |
1447 ) (map pr_classparam classparams) |
1473 ) (map pr_classparam classparams) |
1448 end |
1474 end |
1449 | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = |
1475 | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = |
1450 let |
1476 let |
1451 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1477 val tyvars = CodeName.intro_vars (map fst vs) init_syms; |
1452 fun pr_instdef ((classparam, c_inst), _) = |
1478 fun pr_instdef ((classparam, c_inst), _) = |
1453 semicolon [ |
1479 semicolon [ |
1454 (str o classparam_name class) classparam, |
1480 (str o classparam_name class) classparam, |
1465 str " where {" |
1491 str " where {" |
1466 ], |
1492 ], |
1467 str "};" |
1493 str "};" |
1468 ) (map pr_instdef classparam_insts) |
1494 ) (map pr_instdef classparam_insts) |
1469 end; |
1495 end; |
1470 in pr_def def end; |
1496 in pr_stmt end; |
1471 |
1497 |
1472 fun pretty_haskell_monad c_bind = |
1498 fun pretty_haskell_monad c_bind = |
1473 let |
1499 let |
1474 fun pretty pr vars fxy [(t, _)] = |
1500 fun pretty pr vars fxy [(t, _)] = |
1475 let |
1501 let |
1476 val pr_bind = pr_bind_haskell (K pr); |
1502 val pr_bind = pr_haskell_bind (K pr); |
1477 fun pr_monad (NONE, t) vars = |
1503 fun pr_monad (NONE, t) vars = |
1478 (semicolon [pr vars NOBR t], vars) |
1504 (semicolon [pr vars NOBR t], vars) |
1479 | pr_monad (SOME (bind, true), t) vars = vars |
1505 | pr_monad (SOME (bind, true), t) vars = vars |
1480 |> pr_bind NOBR bind |
1506 |> pr_bind NOBR bind |
1481 |>> (fn p => semicolon [p, str "<-", pr vars NOBR t]) |
1507 |>> (fn p => semicolon [p, str "<-", pr vars NOBR t]) |
1486 val (ps, vars') = fold_map pr_monad binds vars; |
1512 val (ps, vars') = fold_map pr_monad binds vars; |
1487 fun brack p = if fixity BR fxy then Pretty.block [str "(", p, str ")"] else p; |
1513 fun brack p = if fixity BR fxy then Pretty.block [str "(", p, str ")"] else p; |
1488 in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end; |
1514 in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end; |
1489 in (1, pretty) end; |
1515 in (1, pretty) end; |
1490 |
1516 |
1491 end; (*local*) |
1517 fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program = |
1492 |
1518 let |
1493 fun seri_haskell module_prefix module string_classes labelled_name |
1519 val module_alias = if is_some module_name then K module_name else raw_module_alias; |
1494 reserved_syms includes raw_module_alias |
1520 val reserved_names = Name.make_context reserved_names; |
1495 class_syntax tyco_syntax const_syntax code cs seri_dest = |
1521 val mk_name_module = mk_name_module reserved_names module_prefix module_alias program; |
1496 let |
1522 fun add_stmt (name, (stmt, deps)) = |
1497 val is_cons = CodeThingol.is_cons code; |
|
1498 val contr_classparam_typs = CodeThingol.contr_classparam_typs code; |
|
1499 val module_alias = if is_some module then K module else raw_module_alias; |
|
1500 val init_names = Name.make_context reserved_syms; |
|
1501 val name_modl = mk_modl_name_tab init_names module_prefix module_alias code; |
|
1502 fun add_def (name, (def, deps)) = |
|
1503 let |
1523 let |
1504 val (modl, base) = dest_name name; |
1524 val (module_name, base) = dest_name name; |
1505 val name_def = yield_singleton Name.variants; |
1525 val module_name' = mk_name_module module_name; |
1526 val mk_name_stmt = yield_singleton Name.variants; |
|
1506 fun add_fun upper (nsp_fun, nsp_typ) = |
1527 fun add_fun upper (nsp_fun, nsp_typ) = |
1507 let |
1528 let |
1508 val (base', nsp_fun') = |
1529 val (base', nsp_fun') = |
1509 name_def (if upper then first_upper base else base) nsp_fun |
1530 mk_name_stmt (if upper then first_upper base else base) nsp_fun |
1510 in (base', (nsp_fun', nsp_typ)) end; |
1531 in (base', (nsp_fun', nsp_typ)) end; |
1511 fun add_typ (nsp_fun, nsp_typ) = |
1532 fun add_typ (nsp_fun, nsp_typ) = |
1512 let |
1533 let |
1513 val (base', nsp_typ') = name_def (first_upper base) nsp_typ |
1534 val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ |
1514 in (base', (nsp_fun, nsp_typ')) end; |
1535 in (base', (nsp_fun, nsp_typ')) end; |
1515 val add_name = |
1536 val add_name = case stmt |
1516 case def |
1537 of CodeThingol.Fun _ => add_fun false |
1517 of CodeThingol.Fun _ => add_fun false |
1538 | CodeThingol.Datatype _ => add_typ |
1518 | CodeThingol.Datatype _ => add_typ |
1539 | CodeThingol.Datatypecons _ => add_fun true |
1519 | CodeThingol.Datatypecons _ => add_fun true |
1540 | CodeThingol.Class _ => add_typ |
1520 | CodeThingol.Class _ => add_typ |
1541 | CodeThingol.Classrel _ => pair base |
1521 | CodeThingol.Classrel _ => pair base |
1542 | CodeThingol.Classparam _ => add_fun false |
1522 | CodeThingol.Classparam _ => add_fun false |
1543 | CodeThingol.Classinst _ => pair base; |
1523 | CodeThingol.Classinst _ => pair base; |
1544 fun add_stmt' base' = case stmt |
1524 val modlname' = name_modl modl; |
1545 of CodeThingol.Datatypecons _ => |
1525 fun add_def base' = |
1546 cons (name, (NameSpace.append module_name' base', NONE)) |
1526 case def |
1547 | CodeThingol.Classrel _ => I |
1527 of CodeThingol.Datatypecons _ => |
1548 | CodeThingol.Classparam _ => |
1528 cons (name, ((NameSpace.append modlname' base', base'), NONE)) |
1549 cons (name, (NameSpace.append module_name' base', NONE)) |
1529 | CodeThingol.Classrel _ => I |
1550 | _ => cons (name, (NameSpace.append module_name' base', SOME stmt)); |
1530 | CodeThingol.Classparam _ => |
|
1531 cons (name, ((NameSpace.append modlname' base', base'), NONE)) |
|
1532 | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def)); |
|
1533 in |
1551 in |
1534 Symtab.map_default (modlname', ([], ([], (init_names, init_names)))) |
1552 Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names)))) |
1535 (apfst (fold (insert (op = : string * string -> bool)) deps)) |
1553 (apfst (fold (insert (op = : string * string -> bool)) deps)) |
1536 #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname')) |
1554 #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name')) |
1537 #-> (fn (base', names) => |
1555 #-> (fn (base', names) => |
1538 (Symtab.map_entry modlname' o apsnd) (fn (defs, _) => |
1556 (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) => |
1539 (add_def base' defs, names))) |
1557 (add_stmt' base' stmts, names))) |
1540 end; |
1558 end; |
1541 val code' = |
1559 val hs_program = fold add_stmt (AList.make (fn name => |
1542 fold add_def (AList.make (fn name => |
1560 (Graph.get_node program name, Graph.imm_succs program name)) |
1543 (Graph.get_node code name, Graph.imm_succs code name)) |
1561 (Graph.strong_conn program |> flat)) Symtab.empty; |
1544 (Graph.strong_conn code |> flat)) Symtab.empty; |
1562 fun deresolver name = |
1545 val init_syms = CodeName.make_vars reserved_syms; |
1563 (fst o the o AList.lookup (op =) ((fst o snd o the |
1546 fun deresolv name = |
1564 o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name |
1547 (fst o fst o the o AList.lookup (op =) ((fst o snd o the |
|
1548 o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name |
|
1549 handle Option => error ("Unknown statement name: " ^ labelled_name name); |
1565 handle Option => error ("Unknown statement name: " ^ labelled_name name); |
1550 fun deresolv_here name = |
1566 in (deresolver, hs_program) end; |
1551 (snd o fst o the o AList.lookup (op =) ((fst o snd o the |
1567 |
1552 o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name |
1568 fun serialize_haskell module_prefix module_name string_classes labelled_name |
1553 handle Option => error ("Unknown statement name: " ^ labelled_name name); |
1569 reserved_names includes raw_module_alias |
1570 syntax_class syntax_tyco syntax_const program cs destination = |
|
1571 let |
|
1572 val (deresolver, hs_program) = haskell_program_of_program labelled_name |
|
1573 module_name module_prefix reserved_names raw_module_alias program; |
|
1574 val is_cons = CodeThingol.is_cons program; |
|
1575 val contr_classparam_typs = CodeThingol.contr_classparam_typs program; |
|
1554 fun deriving_show tyco = |
1576 fun deriving_show tyco = |
1555 let |
1577 let |
1556 fun deriv _ "fun" = false |
1578 fun deriv _ "fun" = false |
1557 | deriv tycos tyco = member (op =) tycos tyco orelse |
1579 | deriv tycos tyco = member (op =) tycos tyco orelse |
1558 case try (Graph.get_node code) tyco |
1580 case try (Graph.get_node program) tyco |
1559 of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos)) |
1581 of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos)) |
1560 (maps snd cs) |
1582 (maps snd cs) |
1561 | NONE => true |
1583 | NONE => true |
1562 and deriv' tycos (tyco `%% tys) = deriv tycos tyco |
1584 and deriv' tycos (tyco `%% tys) = deriv tycos tyco |
1563 andalso forall (deriv' tycos) tys |
1585 andalso forall (deriv' tycos) tys |
1564 | deriv' _ (ITyVar _) = true |
1586 | deriv' _ (ITyVar _) = true |
1565 in deriv [] tyco end; |
1587 in deriv [] tyco end; |
1566 fun seri_def qualified = pr_haskell class_syntax tyco_syntax |
1588 val reserved_names = CodeName.make_vars reserved_names; |
1567 const_syntax labelled_name init_syms |
1589 fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco |
1568 deresolv_here (if qualified then deresolv else deresolv_here) is_cons |
1590 syntax_const labelled_name reserved_names |
1569 contr_classparam_typs |
1591 (if qualified then deresolver else NameSpace.base o deresolver) |
1592 is_cons contr_classparam_typs |
|
1570 (if string_classes then deriving_show else K false); |
1593 (if string_classes then deriving_show else K false); |
1571 fun assemble_module (modulename, content) = |
1594 fun pr_module name content = |
1572 (modulename, Pretty.chunks [ |
1595 (name, Pretty.chunks [ |
1573 str ("module " ^ modulename ^ " where {"), |
1596 str ("module " ^ name ^ " where {"), |
1574 str "", |
1597 str "", |
1575 content, |
1598 content, |
1576 str "", |
1599 str "", |
1577 str "}" |
1600 str "}" |
1578 ]); |
1601 ]); |
1579 fun seri_module (modlname', (imports, (defs, _))) = |
1602 fun serialize_module (module_name', (deps, (stmts, _))) = |
1580 let |
1603 let |
1581 val imports' = |
1604 val stmt_names = map fst stmts; |
1582 imports |
1605 val deps' = subtract (op =) stmt_names deps |
1583 |> map (name_modl o fst o dest_name) |
|
1584 |> distinct (op =) |
1606 |> distinct (op =) |
1585 |> remove (op =) modlname'; |
1607 |> map_filter (try deresolver); |
1586 val qualified = is_none module andalso |
1608 val qualified = is_none module_name andalso |
1587 imports @ map fst defs |
1609 map deresolver stmt_names @ deps' |
1588 |> distinct (op =) |
|
1589 |> map_filter (try deresolv) |
|
1590 |> map NameSpace.base |
1610 |> map NameSpace.base |
1591 |> has_duplicates (op =); |
1611 |> has_duplicates (op =); |
1592 val mk_import = str o (if qualified |
1612 val imports = deps' |
1613 |> map NameSpace.qualifier |
|
1614 |> distinct (op =); |
|
1615 fun pr_import_include (name, _) = str ("import " ^ name ^ ";"); |
|
1616 val pr_import_module = str o (if qualified |
|
1593 then prefix "import qualified " |
1617 then prefix "import qualified " |
1594 else prefix "import ") o suffix ";"; |
1618 else prefix "import ") o suffix ";"; |
1595 fun import_include (name, _) = str ("import " ^ name ^ ";"); |
|
1596 val content = Pretty.chunks ( |
1619 val content = Pretty.chunks ( |
1597 map mk_import imports' |
1620 map pr_import_include includes |
1598 @ map import_include includes |
1621 @ map pr_import_module imports |
1599 @ str "" |
1622 @ str "" |
1600 :: separate (str "") (map_filter |
1623 :: separate (str "") (map_filter |
1601 (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def)) |
1624 (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt)) |
1602 | (_, (_, NONE)) => NONE) defs) |
1625 | (_, (_, NONE)) => NONE) stmts) |
1603 ) |
1626 ) |
1604 in assemble_module (modlname', content) end; |
1627 in pr_module module_name' content end; |
1605 fun write_module destination (modlname, content) = |
1628 fun write_module destination (modlname, content) = |
1606 let |
1629 let |
1607 val filename = case modlname |
1630 val filename = case modlname |
1608 of "" => Path.explode "Main.hs" |
1631 of "" => Path.explode "Main.hs" |
1609 | _ => (Path.ext "hs" o Path.explode o implode o separate "/" |
1632 | _ => (Path.ext "hs" o Path.explode o implode o separate "/" |
1610 o NameSpace.explode) modlname; |
1633 o NameSpace.explode) modlname; |
1611 val pathname = Path.append destination filename; |
1634 val pathname = Path.append destination filename; |
1612 val _ = File.mkdir (Path.dir pathname); |
1635 val _ = File.mkdir (Path.dir pathname); |
1613 in File.write pathname (target_code_of_pretty content) end |
1636 in File.write pathname (code_of_pretty content) end |
1614 val output = case seri_dest |
1637 fun output Compile = error ("Haskell: no internal compilation") |
1615 of Compile => error ("Haskell: no internal compilation") |
1638 | output Write = K NONE o map (code_writeln o snd) |
1616 | Write => K NONE o map (target_code_writeln o snd) |
1639 | output (File destination) = K NONE o map (write_module destination) |
1617 | File destination => K NONE o map (write_module destination) |
1640 | output String = SOME o cat_lines o map (code_of_pretty o snd); |
1618 | String => SOME o cat_lines o map (target_code_of_pretty o snd); |
1641 in |
1619 in output (map assemble_module includes |
1642 output destination (map (uncurry pr_module) includes |
1620 @ map seri_module (Symtab.dest code')) |
1643 @ map serialize_module (Symtab.dest hs_program)) |
1621 end; |
1644 end; |
1622 |
1645 |
1623 fun isar_seri_haskell module = |
1646 fun isar_seri_haskell module = |
1624 parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) |
1647 parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) |
1625 -- Scan.optional (Args.$$$ "string_classes" >> K true) false |
1648 -- Scan.optional (Args.$$$ "string_classes" >> K true) false |
1626 >> (fn (module_prefix, string_classes) => |
1649 >> (fn (module_prefix, string_classes) => |
1627 seri_haskell module_prefix module string_classes)); |
1650 serialize_haskell module_prefix module string_classes)); |
1628 |
|
1629 |
|
1630 (** diagnosis serializer **) |
|
1631 |
|
1632 fun seri_diagnosis labelled_name _ _ _ _ _ _ code _ _ = |
|
1633 let |
|
1634 val init_names = CodeName.make_vars []; |
|
1635 fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => |
|
1636 brackify_infix (1, R) fxy [ |
|
1637 pr_typ (INFX (1, X)) ty1, |
|
1638 str "->", |
|
1639 pr_typ (INFX (1, R)) ty2 |
|
1640 ]) |
|
1641 | pr_fun _ = NONE |
|
1642 val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names |
|
1643 I I (K false) (K []) (K false); |
|
1644 in |
|
1645 [] |
|
1646 |> Graph.fold (fn (name, (def, _)) => |
|
1647 case try pr (name, def) of SOME p => cons p | NONE => I) code |
|
1648 |> Pretty.chunks2 |
|
1649 |> target_code_of_pretty |
|
1650 |> writeln |
|
1651 |> K NONE |
|
1652 end; |
|
1653 |
1651 |
1654 |
1652 |
1655 (** optional pretty serialization **) |
1653 (** optional pretty serialization **) |
1656 |
1654 |
1657 local |
1655 local |
1809 (fn pretty => fn pr => fn vars => pretty (pr vars)) x; |
1807 (fn pretty => fn pr => fn vars => pretty (pr vars)) x; |
1810 |
1808 |
1811 end; (*local*) |
1809 end; (*local*) |
1812 |
1810 |
1813 |
1811 |
1814 (** user interfaces **) |
1812 (** serializer interfaces **) |
1815 |
1813 |
1816 (* evaluation *) |
1814 (* evaluation *) |
1817 |
1815 |
1818 fun eval_seri module args = |
1816 fun eval_serializer module [] = serialize_ml |
1819 seri_ml (use_text (1, "generated code") Output.ml_output false) |
1817 (use_text (1, "code to be evaluated") Output.ml_output false) |
1820 (fn (cs, SOME s) => "let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end") |
1818 (K Pretty.chunks) pr_sml_stmt |
1821 pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval"); |
1819 (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end")) |
1822 |
1820 (SOME "Isabelle_Eval"); |
1823 fun sml_of thy code cs = get_serializer (K eval_seri) thy target_SML false NONE [] code (SOME cs) String; |
1821 |
1824 |
1822 fun sml_code_of thy program cs = mount_serializer thy (SOME eval_serializer) target_SML NONE [] program cs String |
1825 fun eval thy (ref_name, reff) code (t, ty) args = |
1823 |> the; |
1826 let |
1824 |
1827 val _ = if CodeThingol.contains_dictvar t then |
1825 fun eval eval'' term_of reff thy ct args = |
1828 error "Term to be evaluated constains free dictionaries" else (); |
1826 let |
1829 val code' = CodeThingol.add_value_stmt (t, ty) code; |
1827 val _ = if null (term_frees (term_of ct)) then () else error ("Term " |
1830 val value_code = sml_of thy code' [CodeName.value_name] ; |
1828 ^ quote (Syntax.string_of_term_global thy (term_of ct)) |
1831 val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args); |
1829 ^ " to be evaluated contains free variables"); |
1832 in ML_Context.evaluate Output.ml_output false (ref_name, reff) sml_code end; |
1830 fun eval' program ((vs, ty), t) deps = |
1831 let |
|
1832 val _ = if CodeThingol.contains_dictvar t then |
|
1833 error "Term to be evaluated constains free dictionaries" else (); |
|
1834 val program' = program |
|
1835 |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)])) |
|
1836 |> fold (curry Graph.add_edge CodeName.value_name) deps; |
|
1837 val value_code = sml_code_of thy program' [CodeName.value_name] ; |
|
1838 val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args); |
|
1839 in ML_Context.evaluate Output.ml_output false reff sml_code end; |
|
1840 in eval'' thy (fn t => (t, eval')) ct end; |
|
1841 |
|
1842 fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff; |
|
1843 fun eval_term reff = eval CodeThingol.eval_term I reff; |
|
1844 |
|
1845 |
|
1846 (* presentation *) |
|
1847 |
|
1848 fun code_of thy target module_name cs = |
|
1849 let |
|
1850 val (cs', program) = CodeThingol.consts_program thy cs; |
|
1851 in |
|
1852 string (serialize thy target (SOME module_name) [] program cs') |
|
1853 end; |
|
1833 |
1854 |
1834 |
1855 |
1835 (* infix syntax *) |
1856 (* infix syntax *) |
1836 |
1857 |
1837 datatype 'a mixfix = |
1858 datatype 'a mixfix = |
1875 fun cert_class thy class = |
1896 fun cert_class thy class = |
1876 let |
1897 let |
1877 val _ = AxClass.get_info thy class; |
1898 val _ = AxClass.get_info thy class; |
1878 in class end; |
1899 in class end; |
1879 |
1900 |
1880 fun read_class thy raw_class = |
1901 fun read_class thy = cert_class thy o Sign.intern_class thy; |
1881 let |
|
1882 val class = Sign.intern_class thy raw_class; |
|
1883 val _ = AxClass.get_info thy class; |
|
1884 in class end; |
|
1885 |
1902 |
1886 fun cert_tyco thy tyco = |
1903 fun cert_tyco thy tyco = |
1887 let |
1904 let |
1888 val _ = if Sign.declared_tyname thy tyco then () |
1905 val _ = if Sign.declared_tyname thy tyco then () |
1889 else error ("No such type constructor: " ^ quote tyco); |
1906 else error ("No such type constructor: " ^ quote tyco); |
1890 in tyco end; |
1907 in tyco end; |
1891 |
1908 |
1892 fun read_tyco thy raw_tyco = |
1909 fun read_tyco thy = cert_tyco thy o Sign.intern_type thy; |
1893 let |
|
1894 val tyco = Sign.intern_type thy raw_tyco; |
|
1895 val _ = if Sign.declared_tyname thy tyco then () |
|
1896 else error ("No such type constructor: " ^ quote raw_tyco); |
|
1897 in tyco end; |
|
1898 |
1910 |
1899 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy = |
1911 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy = |
1900 let |
1912 let |
1901 val class = prep_class thy raw_class; |
1913 val class = prep_class thy raw_class; |
1902 val class' = CodeName.class thy class; |
1914 val class' = CodeName.class thy class; |
1969 fun add_reserved target = |
1981 fun add_reserved target = |
1970 let |
1982 let |
1971 fun add sym syms = if member (op =) syms sym |
1983 fun add sym syms = if member (op =) syms sym |
1972 then error ("Reserved symbol " ^ quote sym ^ " already declared") |
1984 then error ("Reserved symbol " ^ quote sym ^ " already declared") |
1973 else insert (op =) sym syms |
1985 else insert (op =) sym syms |
1974 in map_adaptions target o apfst o add end; |
1986 in map_reserved target o add end; |
1975 |
1987 |
1976 fun add_include target = |
1988 fun add_include target = |
1977 let |
1989 let |
1978 fun add (name, SOME content) incls = |
1990 fun add (name, SOME content) incls = |
1979 let |
1991 let |
1981 then warning ("Overwriting existing include " ^ name) |
1993 then warning ("Overwriting existing include " ^ name) |
1982 else (); |
1994 else (); |
1983 in Symtab.update (name, str content) incls end |
1995 in Symtab.update (name, str content) incls end |
1984 | add (name, NONE) incls = |
1996 | add (name, NONE) incls = |
1985 Symtab.delete name incls; |
1997 Symtab.delete name incls; |
1986 in map_adaptions target o apsnd o add end; |
1998 in map_includes target o add end; |
1987 |
1999 |
1988 fun add_modl_alias target = |
2000 fun add_module_alias target = |
1989 map_module_alias target o Symtab.update o apsnd CodeName.check_modulename; |
2001 map_module_alias target o Symtab.update o apsnd CodeName.check_modulename; |
1990 |
2002 |
1991 fun add_monad target c_run c_bind c_return_unit thy = |
2003 fun add_monad target raw_c_run raw_c_bind raw_c_return_unit thy = |
1992 let |
2004 let |
1993 val c_run' = CodeUnit.read_const thy c_run; |
2005 val c_run = CodeUnit.read_const thy raw_c_run; |
1994 val c_bind' = CodeUnit.read_const thy c_bind; |
2006 val c_bind = CodeUnit.read_const thy raw_c_bind; |
1995 val c_bind'' = CodeName.const thy c_bind'; |
2007 val c_bind' = CodeName.const thy c_bind; |
1996 val c_return_unit'' = (Option.map o pairself) |
2008 val c_return_unit' = (Option.map o pairself) |
1997 (CodeName.const thy o CodeUnit.read_const thy) c_return_unit; |
2009 (CodeName.const thy o CodeUnit.read_const thy) raw_c_return_unit; |
1998 val is_haskell = target = target_Haskell; |
2010 val is_haskell = target = target_Haskell; |
1999 val _ = if is_haskell andalso is_some c_return_unit'' |
2011 val _ = if is_haskell andalso is_some c_return_unit' |
2000 then error ("No unit entry may be given for Haskell monad") |
2012 then error ("No unit entry may be given for Haskell monad") |
2001 else (); |
2013 else (); |
2002 val _ = if not is_haskell andalso is_none c_return_unit'' |
2014 val _ = if not is_haskell andalso is_none c_return_unit' |
2003 then error ("Unit entry must be given for SML/OCaml monad") |
2015 then error ("Unit entry must be given for SML/OCaml monad") |
2004 else (); |
2016 else (); |
2005 in if target = target_Haskell then |
2017 in if target = target_Haskell then |
2006 thy |
2018 thy |
2007 |> gen_add_syntax_const (K I) target_Haskell c_run' |
2019 |> gen_add_syntax_const (K I) target_Haskell c_run |
2008 (SOME (pretty_haskell_monad c_bind'')) |
2020 (SOME (pretty_haskell_monad c_bind')) |
2009 |> gen_add_syntax_const (K I) target_Haskell c_bind' |
2021 |> gen_add_syntax_const (K I) target_Haskell c_bind |
2010 (no_bindings (SOME (parse_infix fst (L, 1) ">>="))) |
2022 (no_bindings (SOME (parse_infix fst (L, 1) ">>="))) |
2011 else |
2023 else |
2012 thy |
2024 thy |
2013 |> gen_add_syntax_const (K I) target c_bind' |
2025 |> gen_add_syntax_const (K I) target c_bind |
2014 (SOME (pretty_imperative_monad_bind c_bind'' |
2026 (SOME (pretty_imperative_monad_bind c_bind' |
2015 ((fst o the) c_return_unit'') ((snd o the) c_return_unit''))) |
2027 ((fst o the) c_return_unit') ((snd o the) c_return_unit'))) |
2016 end; |
2028 end; |
2017 |
2029 |
2018 fun gen_allow_exception prep_cs raw_c thy = |
2030 fun gen_allow_abort prep_cs raw_c thy = |
2019 let |
2031 let |
2020 val c = prep_cs thy raw_c; |
2032 val c = prep_cs thy raw_c; |
2021 val c' = CodeName.const thy c; |
2033 val c' = CodeName.const thy c; |
2022 in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end; |
2034 in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end; |
2023 |
2035 |
2026 #-> (fn y => |
2038 #-> (fn y => |
2027 fold_map (fn x => g |-- f >> pair x) xs |
2039 fold_map (fn x => g |-- f >> pair x) xs |
2028 #-> (fn xys => pair ((x, y) :: xys))); |
2040 #-> (fn xys => pair ((x, y) :: xys))); |
2029 |
2041 |
2030 |
2042 |
2031 (* conrete syntax *) |
2043 (* concrete syntax *) |
2032 |
2044 |
2033 structure P = OuterParse |
2045 structure P = OuterParse |
2034 and K = OuterKeyword |
2046 and K = OuterKeyword |
2035 |
2047 |
2036 fun parse_multi_syntax parse_thing parse_syntax = |
2048 fun parse_multi_syntax parse_thing parse_syntax = |
2074 |
2086 |
2075 val add_syntax_class = gen_add_syntax_class cert_class (K I); |
2087 val add_syntax_class = gen_add_syntax_class cert_class (K I); |
2076 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco; |
2088 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco; |
2077 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco; |
2089 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco; |
2078 val add_syntax_const = gen_add_syntax_const (K I); |
2090 val add_syntax_const = gen_add_syntax_const (K I); |
2079 val allow_exception = gen_allow_exception (K I); |
2091 val allow_abort = gen_allow_abort (K I); |
2080 |
2092 |
2081 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const; |
2093 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const; |
2082 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco; |
2094 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco; |
2083 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco; |
2095 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco; |
2084 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const; |
2096 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const; |
2085 val allow_exception_cmd = gen_allow_exception CodeUnit.read_const; |
2097 val allow_abort_cmd = gen_allow_abort CodeUnit.read_const; |
2086 |
2098 |
2087 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco; |
2099 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco; |
2088 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings); |
2100 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings); |
2089 |
2101 |
2090 fun add_undefined target undef target_undefined thy = |
2102 fun add_undefined target undef target_undefined thy = |
2150 thy |
2162 thy |
2151 |> add_syntax_const target str (SOME pr) |
2163 |> add_syntax_const target str (SOME pr) |
2152 end; |
2164 end; |
2153 |
2165 |
2154 |
2166 |
2155 (* Isar commands *) |
2167 (** code generation at a glance **) |
2156 |
2168 |
2157 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK]; |
2169 fun read_const_exprs thy cs = |
2170 let |
|
2171 val (cs1, cs2) = CodeName.read_const_exprs thy cs; |
|
2172 val (cs3, program) = CodeThingol.consts_program thy cs2; |
|
2173 val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy); |
|
2174 val cs5 = map_filter |
|
2175 (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3); |
|
2176 in fold (insert (op =)) cs5 cs1 end; |
|
2177 |
|
2178 fun cached_program thy = |
|
2179 let |
|
2180 val program = CodeThingol.cached_program thy; |
|
2181 in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end |
|
2182 |
|
2183 fun code thy cs seris = |
|
2184 let |
|
2185 val (cs', program) = if null cs |
|
2186 then cached_program thy |
|
2187 else CodeThingol.consts_program thy cs; |
|
2188 fun mk_seri_dest dest = case dest |
|
2189 of NONE => compile |
|
2190 | SOME "-" => write |
|
2191 | SOME f => file (Path.explode f) |
|
2192 val _ = map (fn (((target, module), dest), args) => |
|
2193 (mk_seri_dest dest (serialize thy target module args program cs'))) seris; |
|
2194 in () end; |
|
2195 |
|
2196 fun sml_of thy cs = |
|
2197 let |
|
2198 val (cs', program) = CodeThingol.consts_program thy cs; |
|
2199 in sml_code_of thy program cs' ^ " ()" end; |
|
2200 |
|
2201 fun code_antiq (ctxt, args) = |
|
2202 let |
|
2203 val thy = Context.theory_of ctxt; |
|
2204 val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args); |
|
2205 val cs = map (CodeUnit.check_const thy) ts; |
|
2206 val s = sml_of thy cs; |
|
2207 in (("codevals", s), (ctxt', args')) end; |
|
2208 |
|
2209 fun export_code_cmd raw_cs seris thy = code thy (read_const_exprs thy raw_cs) seris; |
|
2210 |
|
2211 val (inK, module_nameK, fileK) = ("in", "module_name", "file"); |
|
2212 |
|
2213 fun code_exprP cmd = |
|
2214 (Scan.repeat P.term |
|
2215 -- Scan.repeat (P.$$$ inK |-- P.name |
|
2216 -- Scan.option (P.$$$ module_nameK |-- P.name) |
|
2217 -- Scan.option (P.$$$ fileK |-- P.name) |
|
2218 -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") [] |
|
2219 ) >> (fn (raw_cs, seris) => cmd raw_cs seris)); |
|
2220 |
|
2221 |
|
2222 (** Isar setup **) |
|
2223 |
|
2224 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK]; |
|
2158 |
2225 |
2159 val _ = |
2226 val _ = |
2160 OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl ( |
2227 OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl ( |
2161 parse_multi_syntax P.xname |
2228 parse_multi_syntax P.xname |
2162 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 |
2229 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 |
2209 ); |
2276 ); |
2210 |
2277 |
2211 val _ = |
2278 val _ = |
2212 OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl ( |
2279 OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl ( |
2213 P.name -- Scan.repeat1 (P.name -- P.name) |
2280 P.name -- Scan.repeat1 (P.name -- P.name) |
2214 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames) |
2281 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames) |
2215 ); |
2282 ); |
2216 |
2283 |
2217 val _ = |
2284 val _ = |
2218 OuterSyntax.command "code_exception" "permit exceptions for constant" K.thy_decl ( |
2285 OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl ( |
2219 Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd) |
2286 Scan.repeat1 P.term >> (Toplevel.theory o fold allow_abort_cmd) |
2220 ); |
2287 ); |
2221 |
2288 |
2289 val _ = |
|
2290 OuterSyntax.command "export_code" "generate executable code for constants" |
|
2291 K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
|
2292 |
|
2293 fun shell_command thyname cmd = Toplevel.program (fn _ => |
|
2294 (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
|
2295 of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
|
2296 | NONE => error ("Bad directive " ^ quote cmd))) |
|
2297 handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
|
2298 |
|
2299 val _ = ML_Context.value_antiq "code" code_antiq; |
|
2300 |
|
2222 |
2301 |
2223 (* serializer setup, including serializer defaults *) |
2302 (* serializer setup, including serializer defaults *) |
2224 |
2303 |
2225 val setup = |
2304 val setup = |
2226 add_serializer (target_SML, isar_seri_sml) |
2305 add_target (target_SML, isar_seri_sml) |
2227 #> add_serializer (target_OCaml, isar_seri_ocaml) |
2306 #> add_target (target_OCaml, isar_seri_ocaml) |
2228 #> add_serializer (target_Haskell, isar_seri_haskell) |
2307 #> add_target (target_Haskell, isar_seri_haskell) |
2229 #> add_serializer (target_diag, fn _ => fn _=> seri_diagnosis) |
|
2230 #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => |
2308 #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => |
2231 brackify_infix (1, R) fxy [ |
2309 brackify_infix (1, R) fxy [ |
2232 pr_typ (INFX (1, X)) ty1, |
2310 pr_typ (INFX (1, X)) ty1, |
2233 str "->", |
2311 str "->", |
2234 pr_typ (INFX (1, R)) ty2 |
2312 pr_typ (INFX (1, R)) ty2 |