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
|
|
|
|
|
|
|
|
let dummy_pretty = pretty
|
|
|
|
|
|
|
|
instance pretty prettyable begin
|
|
|
|
let pretty x w =
|
|
|
|
match x with
|
|
|
|
| S a -> show a
|
|
|
|
| P a -> dummy_pretty a w
|
|
|
|
end
|
|
|
|
|
|
|
|
class prettyrecord 'r begin
|
|
|
|
val name : 'r -> string
|
|
|
|
val fields : 'r -> list (string * prettyable)
|
|
|
|
end
|
|
|
|
|
|
|
|
instance prettyrecord 'a => pretty 'a begin
|
|
|
|
let pretty 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 rec field_str acc l =
|
|
|
|
match l with
|
|
|
|
| [] -> acc
|
|
|
|
| Cons ((name, field), xs) -> field_str (acc ^ prep ^ " " ^ name ^ " = " ^ (pretty field x) ^ ",\n") xs
|
|
|
|
let body = field_str "" rf
|
|
|
|
(name a) ^ " {\n" ^ body ^ prep ^ "}"
|
|
|
|
end
|