Currently, the pretty-printer doesn't indent long expressions. Indenting them would improve readability.
An example of the current output:
function snap$Binop(self: Ref): Binop$Snap
requires acc(Binop(self), read())
{
(unfolding acc(Binop(self), read()) in (self.discriminant == 1 ? (unfolding acc(BinopSub(self.enum_Sub), read()) in (unfolding acc(u32(self.enum_Sub.f$1), read()) in (unfolding acc(u32(self.enum_Sub.f$0), read()) in get$1$Binop$Snap(self.enum_Sub.f$0.val_int, self.enum_Sub.f$1.val_int)))) : (unfolding acc(BinopAdd(self.enum_Add), read()) in (unfolding acc(u32(self.enum_Add.f$1), read()) in (unfolding acc(u32(self.enum_Add.f$0), read()) in get$0$Binop$Snap(self.enum_Add.f$0.val_int, self.enum_Add.f$1.val_int))))))
}
A more readable output:
function snap$Binop(self: Ref): Binop$Snap
requires acc(Binop(self), read())
{
(unfolding acc(Binop(self), read()) in
(self.discriminant == 1 ?
(unfolding acc(BinopSub(self.enum_Sub), read()) in
(unfolding acc(u32(self.enum_Sub.f$1), read()) in
(unfolding acc(u32(self.enum_Sub.f$0), read()) in
get$1$Binop$Snap(self.enum_Sub.f$0.val_int, self.enum_Sub.f$1.val_int)
)
)
) :
(unfolding acc(BinopAdd(self.enum_Add), read()) in
(unfolding acc(u32(self.enum_Add.f$1), read()) in
(unfolding acc(u32(self.enum_Add.f$0), read()) in
get$0$Binop$Snap(self.enum_Add.f$0.val_int, self.enum_Add.f$1.val_int)
)
)
)
)
)
}
Currently, the pretty-printer doesn't indent long expressions. Indenting them would improve readability.
An example of the current output:
A more readable output: