48 val pr_label_classrel = translate_string (fn "." => "__" | c => c) |
48 val pr_label_classrel = translate_string (fn "." => "__" | c => c) |
49 o Long_Name.qualifier; |
49 o Long_Name.qualifier; |
50 val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier; |
50 val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier; |
51 fun pr_dicts fxy ds = |
51 fun pr_dicts fxy ds = |
52 let |
52 let |
53 fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_" |
53 fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_" |
54 | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_"; |
54 | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_"; |
55 fun pr_proj [] p = |
55 fun pr_proj [] p = |
56 p |
56 p |
57 | pr_proj [p'] p = |
57 | pr_proj [p'] p = |
58 brackets [p', p] |
58 brackets [p', p] |
59 | pr_proj (ps as _ :: _) p = |
59 | pr_proj (ps as _ :: _) p = |
85 | SOME (i, pr) => pr pr_typ fxy tys) |
85 | SOME (i, pr) => pr pr_typ fxy tys) |
86 | pr_typ fxy (ITyVar v) = str ("'" ^ v); |
86 | pr_typ fxy (ITyVar v) = str ("'" ^ v); |
87 fun pr_term is_closure thm vars fxy (IConst c) = |
87 fun pr_term is_closure thm vars fxy (IConst c) = |
88 pr_app is_closure thm vars fxy (c, []) |
88 pr_app is_closure thm vars fxy (c, []) |
89 | pr_term is_closure thm vars fxy (IVar v) = |
89 | pr_term is_closure thm vars fxy (IVar v) = |
90 str (Code_Name.lookup_var vars v) |
90 str (Code_Printer.lookup_var vars v) |
91 | pr_term is_closure thm vars fxy (t as t1 `$ t2) = |
91 | pr_term is_closure thm vars fxy (t as t1 `$ t2) = |
92 (case Code_Thingol.unfold_const_app t |
92 (case Code_Thingol.unfold_const_app t |
93 of SOME c_ts => pr_app is_closure thm vars fxy c_ts |
93 of SOME c_ts => pr_app is_closure thm vars fxy c_ts |
94 | NONE => brackify fxy |
94 | NONE => brackify fxy |
95 [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) |
95 [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) |
180 val consts = map_filter |
180 val consts = map_filter |
181 (fn c => if (is_some o syntax_const) c |
181 (fn c => if (is_some o syntax_const) c |
182 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
182 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
183 (Code_Thingol.fold_constnames (insert (op =)) t []); |
183 (Code_Thingol.fold_constnames (insert (op =)) t []); |
184 val vars = reserved_names |
184 val vars = reserved_names |
185 |> Code_Name.intro_vars consts; |
185 |> Code_Printer.intro_vars consts; |
186 in |
186 in |
187 concat [ |
187 concat [ |
188 str "val", |
188 str "val", |
189 (str o deresolve) name, |
189 (str o deresolve) name, |
190 str ":", |
190 str ":", |
205 val consts = map_filter |
205 val consts = map_filter |
206 (fn c => if (is_some o syntax_const) c |
206 (fn c => if (is_some o syntax_const) c |
207 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
207 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
208 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); |
208 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); |
209 val vars = reserved_names |
209 val vars = reserved_names |
210 |> Code_Name.intro_vars consts |
210 |> Code_Printer.intro_vars consts |
211 |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) |
211 |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) |
212 (insert (op =)) ts []); |
212 (insert (op =)) ts []); |
213 in |
213 in |
214 concat ( |
214 concat ( |
215 str definer |
215 str definer |
216 :: (str o deresolve) name |
216 :: (str o deresolve) name |
264 val (ps, p) = split_last |
264 val (ps, p) = split_last |
265 (pr_data "datatype" data :: map (pr_data "and") datas'); |
265 (pr_data "datatype" data :: map (pr_data "and") datas'); |
266 in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end |
266 in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end |
267 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = |
267 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = |
268 let |
268 let |
269 val w = Code_Name.first_upper v ^ "_"; |
269 val w = Code_Printer.first_upper v ^ "_"; |
270 fun pr_superclass_field (class, classrel) = |
270 fun pr_superclass_field (class, classrel) = |
271 (concat o map str) [ |
271 (concat o map str) [ |
272 pr_label_classrel classrel, ":", "'" ^ v, deresolve class |
272 pr_label_classrel classrel, ":", "'" ^ v, deresolve class |
273 ]; |
273 ]; |
274 fun pr_classparam_field (classparam, ty) = |
274 fun pr_classparam_field (classparam, ty) = |
360 |
360 |
361 fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = |
361 fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = |
362 let |
362 let |
363 fun pr_dicts fxy ds = |
363 fun pr_dicts fxy ds = |
364 let |
364 let |
365 fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v |
365 fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v |
366 | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1); |
366 | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1); |
367 fun pr_proj ps p = |
367 fun pr_proj ps p = |
368 fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p |
368 fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p |
369 fun pr_dict fxy (DictConst (inst, dss)) = |
369 fun pr_dict fxy (DictConst (inst, dss)) = |
370 brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss) |
370 brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss) |
371 | pr_dict fxy (DictVar (classrels, v)) = |
371 | pr_dict fxy (DictVar (classrels, v)) = |
393 | SOME (i, pr) => pr pr_typ fxy tys) |
393 | SOME (i, pr) => pr pr_typ fxy tys) |
394 | pr_typ fxy (ITyVar v) = str ("'" ^ v); |
394 | pr_typ fxy (ITyVar v) = str ("'" ^ v); |
395 fun pr_term is_closure thm vars fxy (IConst c) = |
395 fun pr_term is_closure thm vars fxy (IConst c) = |
396 pr_app is_closure thm vars fxy (c, []) |
396 pr_app is_closure thm vars fxy (c, []) |
397 | pr_term is_closure thm vars fxy (IVar v) = |
397 | pr_term is_closure thm vars fxy (IVar v) = |
398 str (Code_Name.lookup_var vars v) |
398 str (Code_Printer.lookup_var vars v) |
399 | pr_term is_closure thm vars fxy (t as t1 `$ t2) = |
399 | pr_term is_closure thm vars fxy (t as t1 `$ t2) = |
400 (case Code_Thingol.unfold_const_app t |
400 (case Code_Thingol.unfold_const_app t |
401 of SOME c_ts => pr_app is_closure thm vars fxy c_ts |
401 of SOME c_ts => pr_app is_closure thm vars fxy c_ts |
402 | NONE => |
402 | NONE => |
403 brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) |
403 brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) |
466 | fillup_param x (i, NONE) = x ^ string_of_int i; |
466 | fillup_param x (i, NONE) = x ^ string_of_int i; |
467 val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE); |
467 val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE); |
468 val x = Name.variant (map_filter I fished1) "x"; |
468 val x = Name.variant (map_filter I fished1) "x"; |
469 val fished2 = map_index (fillup_param x) fished1; |
469 val fished2 = map_index (fillup_param x) fished1; |
470 val (fished3, _) = Name.variants fished2 Name.context; |
470 val (fished3, _) = Name.variants fished2 Name.context; |
471 val vars' = Code_Name.intro_vars fished3 vars; |
471 val vars' = Code_Printer.intro_vars fished3 vars; |
472 in map (Code_Name.lookup_var vars') fished3 end; |
472 in map (Code_Printer.lookup_var vars') fished3 end; |
473 fun pr_stmt (MLExc (name, n)) = |
473 fun pr_stmt (MLExc (name, n)) = |
474 let |
474 let |
475 val exc_str = |
475 val exc_str = |
476 (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; |
476 (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; |
477 in |
477 in |
489 val consts = map_filter |
489 val consts = map_filter |
490 (fn c => if (is_some o syntax_const) c |
490 (fn c => if (is_some o syntax_const) c |
491 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
491 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
492 (Code_Thingol.fold_constnames (insert (op =)) t []); |
492 (Code_Thingol.fold_constnames (insert (op =)) t []); |
493 val vars = reserved_names |
493 val vars = reserved_names |
494 |> Code_Name.intro_vars consts; |
494 |> Code_Printer.intro_vars consts; |
495 in |
495 in |
496 concat [ |
496 concat [ |
497 str "let", |
497 str "let", |
498 (str o deresolve) name, |
498 (str o deresolve) name, |
499 str ":", |
499 str ":", |
509 val consts = map_filter |
509 val consts = map_filter |
510 (fn c => if (is_some o syntax_const) c |
510 (fn c => if (is_some o syntax_const) c |
511 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
511 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
512 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); |
512 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); |
513 val vars = reserved_names |
513 val vars = reserved_names |
514 |> Code_Name.intro_vars consts |
514 |> Code_Printer.intro_vars consts |
515 |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) |
515 |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) |
516 (insert (op =)) ts []); |
516 (insert (op =)) ts []); |
517 in concat [ |
517 in concat [ |
518 (Pretty.block o Pretty.commas) |
518 (Pretty.block o Pretty.commas) |
519 (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts), |
519 (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts), |
520 str "->", |
520 str "->", |
525 val consts = map_filter |
525 val consts = map_filter |
526 (fn c => if (is_some o syntax_const) c |
526 (fn c => if (is_some o syntax_const) c |
527 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
527 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
528 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); |
528 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); |
529 val vars = reserved_names |
529 val vars = reserved_names |
530 |> Code_Name.intro_vars consts |
530 |> Code_Printer.intro_vars consts |
531 |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) |
531 |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) |
532 (insert (op =)) ts []); |
532 (insert (op =)) ts []); |
533 in |
533 in |
534 concat ( |
534 concat ( |
535 (if is_pseudo then [str "()"] |
535 (if is_pseudo then [str "()"] |
536 else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts) |
536 else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts) |
554 (fn c => if (is_some o syntax_const) c |
554 (fn c => if (is_some o syntax_const) c |
555 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
555 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
556 ((fold o Code_Thingol.fold_constnames) |
556 ((fold o Code_Thingol.fold_constnames) |
557 (insert (op =)) (map (snd o fst) eqs) []); |
557 (insert (op =)) (map (snd o fst) eqs) []); |
558 val vars = reserved_names |
558 val vars = reserved_names |
559 |> Code_Name.intro_vars consts; |
559 |> Code_Printer.intro_vars consts; |
560 val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs; |
560 val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs; |
561 in |
561 in |
562 Pretty.block ( |
562 Pretty.block ( |
563 Pretty.breaks dummy_parms |
563 Pretty.breaks dummy_parms |
564 @ Pretty.brk 1 |
564 @ Pretty.brk 1 |
621 val (ps, p) = split_last |
621 val (ps, p) = split_last |
622 (pr_data "type" data :: map (pr_data "and") datas'); |
622 (pr_data "type" data :: map (pr_data "and") datas'); |
623 in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end |
623 in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end |
624 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = |
624 | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = |
625 let |
625 let |
626 val w = "_" ^ Code_Name.first_upper v; |
626 val w = "_" ^ Code_Printer.first_upper v; |
627 fun pr_superclass_field (class, classrel) = |
627 fun pr_superclass_field (class, classrel) = |
628 (concat o map str) [ |
628 (concat o map str) [ |
629 deresolve classrel, ":", "'" ^ v, deresolve class |
629 deresolve classrel, ":", "'" ^ v, deresolve class |
630 ]; |
630 ]; |
631 fun pr_classparam_field (classparam, ty) = |
631 fun pr_classparam_field (classparam, ty) = |
763 in (x, (nsp_fun', nsp_typ)) end; |
763 in (x, (nsp_fun', nsp_typ)) end; |
764 fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = |
764 fun map_nsp_typ_yield f (nsp_fun, nsp_typ) = |
765 let |
765 let |
766 val (x, nsp_typ') = f nsp_typ |
766 val (x, nsp_typ') = f nsp_typ |
767 in (x, (nsp_fun, nsp_typ')) end; |
767 in (x, (nsp_fun, nsp_typ')) end; |
768 val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program; |
768 val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program; |
769 fun mk_name_stmt upper name nsp = |
769 fun mk_name_stmt upper name nsp = |
770 let |
770 let |
771 val (_, base) = Code_Name.dest_name name; |
771 val (_, base) = Code_Printer.dest_name name; |
772 val base' = if upper then Code_Name.first_upper base else base; |
772 val base' = if upper then Code_Printer.first_upper base else base; |
773 val ([base''], nsp') = Name.variants [base'] nsp; |
773 val ([base''], nsp') = Name.variants [base'] nsp; |
774 in (base'', nsp') end; |
774 in (base'', nsp') end; |
775 fun rearrange_fun name (tysm as (vs, ty), raw_eqs) = |
775 fun rearrange_fun name (tysm as (vs, ty), raw_eqs) = |
776 let |
776 let |
777 val eqs = filter (snd o snd) raw_eqs; |
777 val eqs = filter (snd o snd) raw_eqs; |
851 val names as (name :: names') = map fst stmts; |
851 val names as (name :: names') = map fst stmts; |
852 val deps = |
852 val deps = |
853 [] |
853 [] |
854 |> fold (fold (insert (op =)) o Graph.imm_succs program) names |
854 |> fold (fold (insert (op =)) o Graph.imm_succs program) names |
855 |> subtract (op =) names; |
855 |> subtract (op =) names; |
856 val (module_names, _) = (split_list o map Code_Name.dest_name) names; |
856 val (module_names, _) = (split_list o map Code_Printer.dest_name) names; |
857 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names |
857 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names |
858 handle Empty => |
858 handle Empty => |
859 error ("Different namespace prefixes for mutual dependencies:\n" |
859 error ("Different namespace prefixes for mutual dependencies:\n" |
860 ^ commas (map labelled_name names) |
860 ^ commas (map labelled_name names) |
861 ^ "\n" |
861 ^ "\n" |
862 ^ commas module_names); |
862 ^ commas module_names); |
863 val module_name_path = Long_Name.explode module_name; |
863 val module_name_path = Long_Name.explode module_name; |
864 fun add_dep name name' = |
864 fun add_dep name name' = |
865 let |
865 let |
866 val module_name' = (mk_name_module o fst o Code_Name.dest_name) name'; |
866 val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name'; |
867 in if module_name = module_name' then |
867 in if module_name = module_name' then |
868 map_node module_name_path (Graph.add_edge (name, name')) |
868 map_node module_name_path (Graph.add_edge (name, name')) |
869 else let |
869 else let |
870 val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =) |
870 val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =) |
871 (module_name_path, Long_Name.explode module_name'); |
871 (module_name_path, Long_Name.explode module_name'); |
889 val (_, nodes) = empty_module |
889 val (_, nodes) = empty_module |
890 |> fold add_stmts' (map (AList.make (Graph.get_node program)) |
890 |> fold add_stmts' (map (AList.make (Graph.get_node program)) |
891 (rev (Graph.strong_conn program))); |
891 (rev (Graph.strong_conn program))); |
892 fun deresolver prefix name = |
892 fun deresolver prefix name = |
893 let |
893 let |
894 val module_name = (fst o Code_Name.dest_name) name; |
894 val module_name = (fst o Code_Printer.dest_name) name; |
895 val module_name' = (Long_Name.explode o mk_name_module) module_name; |
895 val module_name' = (Long_Name.explode o mk_name_module) module_name; |
896 val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); |
896 val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); |
897 val stmt_name = |
897 val stmt_name = |
898 nodes |
898 nodes |
899 |> fold (fn name => fn node => case Graph.get_node node name |
899 |> fold (fn name => fn node => case Graph.get_node node name |
912 val is_cons = Code_Thingol.is_cons program; |
912 val is_cons = Code_Thingol.is_cons program; |
913 val stmt_names = Code_Target.stmt_names_of_destination destination; |
913 val stmt_names = Code_Target.stmt_names_of_destination destination; |
914 val module_name = if null stmt_names then raw_module_name else SOME "Code"; |
914 val module_name = if null stmt_names then raw_module_name else SOME "Code"; |
915 val (deresolver, nodes) = ml_node_of_program labelled_name module_name |
915 val (deresolver, nodes) = ml_node_of_program labelled_name module_name |
916 reserved_names raw_module_alias program; |
916 reserved_names raw_module_alias program; |
917 val reserved_names = Code_Name.make_vars reserved_names; |
917 val reserved_names = Code_Printer.make_vars reserved_names; |
918 fun pr_node prefix (Dummy _) = |
918 fun pr_node prefix (Dummy _) = |
919 NONE |
919 NONE |
920 | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse |
920 | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse |
921 (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME |
921 (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME |
922 (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names |
922 (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names |