2021-03-09 03:55:25 +00:00
|
|
|
open import "prelude.ml"
|
|
|
|
|
|
|
|
class pretty 'a begin
|
|
|
|
val pretty : 'a -> int -> string
|
|
|
|
end
|
2021-03-09 17:55:22 +00:00
|
|
|
|
|
|
|
type prettyable =
|
|
|
|
| S : show 'a => 'a -> prettyable
|
|
|
|
| P : pretty 'a => 'a -> prettyable
|
|
|
|
|
2021-03-10 00:01:09 +00:00
|
|
|
let render_prettyable x w =
|
|
|
|
match x with
|
|
|
|
| S a -> show a
|
|
|
|
| P a -> pretty a w
|
2021-03-09 17:55:22 +00:00
|
|
|
|
|
|
|
class prettyrecord 'r begin
|
|
|
|
val name : 'r -> string
|
|
|
|
val fields : 'r -> list (string * prettyable)
|
|
|
|
end
|
|
|
|
|
2021-03-10 00:01:09 +00:00
|
|
|
let pretty_from_record a w =
|
|
|
|
let rec smul s n =
|
|
|
|
if n <= 0 then
|
|
|
|
""
|
|
|
|
else
|
|
|
|
s ^ (smul s (n - 1))
|
|
|
|
let x = w + 2
|
|
|
|
let prep = smul " " w
|
|
|
|
let rf = fields a
|
|
|
|
let render_field (name, field) =
|
|
|
|
name ^ " = " ^ (render_prettyable field x)
|
|
|
|
let field_str =
|
|
|
|
foldl (fun acc f -> acc ^ prep ^ " " ^ (render_field f) ^ ",\n") ""
|
|
|
|
let body = field_str rf
|
|
|
|
(name a) ^ " {\n" ^ body ^ prep ^ "}"
|