442 vars |
442 vars |
443 |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) |
443 |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) |
444 |>> (fn p => concat |
444 |>> (fn p => concat |
445 [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"]) |
445 [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"]) |
446 val (ps, vars') = fold_map pr binds vars; |
446 val (ps, vars') = fold_map pr binds vars; |
447 in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR body) end |
447 fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps; |
|
448 in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end |
448 | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) = |
449 | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) = |
449 let |
450 let |
450 fun pr delim (pat, body) = |
451 fun pr delim (pat, body) = |
451 let |
452 let |
452 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; |
453 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; |
647 in Pretty.chunks ( |
648 in Pretty.chunks ( |
648 concat [ |
649 concat [ |
649 str ("type '" ^ v), |
650 str ("type '" ^ v), |
650 (str o deresolve) class, |
651 (str o deresolve) class, |
651 str "=", |
652 str "=", |
652 enum_default "();;" ";" "{" "};;" ( |
653 enum_default "unit;;" ";" "{" "};;" ( |
653 map pr_superclass_field superclasses |
654 map pr_superclass_field superclasses |
654 @ map pr_classparam_field classparams |
655 @ map pr_classparam_field classparams |
655 ) |
656 ) |
656 ] |
657 ] |
657 :: map pr_classparam_proj classparams |
658 :: map pr_classparam_proj classparams |
706 let |
707 let |
707 val i = ord c; |
708 val i = ord c; |
708 val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126 |
709 val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126 |
709 then chr i else c |
710 then chr i else c |
710 in s end; |
711 in s end; |
|
712 fun bignum_ocaml k = if k <= 1073741823 |
|
713 then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" |
|
714 else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")" |
711 in Literals { |
715 in Literals { |
712 literal_char = enclose "'" "'" o char_ocaml, |
716 literal_char = enclose "'" "'" o char_ocaml, |
713 literal_string = quote o translate_string char_ocaml, |
717 literal_string = quote o translate_string char_ocaml, |
714 literal_numeral = fn unbounded => fn k => if k >= 0 then |
718 literal_numeral = fn unbounded => fn k => if k >= 0 then |
715 if unbounded then |
719 if unbounded then bignum_ocaml k |
716 "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" |
|
717 else string_of_int k |
720 else string_of_int k |
718 else |
721 else |
719 if unbounded then |
722 if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")" |
720 "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-" |
|
721 o string_of_int o op ~) k ^ ")" |
|
722 else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k, |
723 else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k, |
723 literal_list = Pretty.enum ";" "[" "]", |
724 literal_list = Pretty.enum ";" "[" "]", |
724 infix_cons = (6, "::") |
725 infix_cons = (6, "::") |
725 } end; |
726 } end; |
726 |
727 |