What is the `cls` sort seen in `basics_pre.sats`?

[Yannick Duchêne]

In `basics_pre.sats`, line #301 to line #315, is this:

stacst lte_cls_cls : (cls, cls) -> bool
stacst gte_cls_cls : (cls, cls) -> bool
stadef <= = lte_cls_cls
stadef >= = gte_cls_cls
//
stadef
lterel_cls_cls
(
  c1: cls, c2: cls, lterel_cls_cls_res: bool
) : bool = lterel_cls_cls_res
stadef
gterel_cls_cls
(
  c1: cls, c2: cls, gterel_cls_cls_res: bool
) : bool = gterel_cls_cls_res

As it's not defined in any file (or I missed it), this must be a built-in sort. What is this `cls` sort?

[gmhwxi]

This one is for building interface for OOP.

[William Blair]

A good example of using the `cls` sort for doing OOP is the ATS library for GTK. In that code, the `cls` sort is used to make the ATS types for GTK Objects more precise.

    https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/GTK

For example, it's my understanding that values in the GTK C library are references to glib objects. With the cls sort, you could describe the following hierarchy for GTK Objects.

    classdec GtkObject : GInitiallyUnowned
       classdec GtkWidget_cls : GtkObject
         classdec GtkMisc_cls : GtkWidget_cls
           classdec GtkLabel_cls : GtkMisc_cls
           classdec GtkArrow_cls : GtkMisc_cls
           // end of [GtkMisc]

This makes GtkWidget a subclass of GtkObject, and GtkMisc a subclass of GtkWidget, and so on.

If we wanted to make a dynamic type that would be used only for GTKWidgets, we could declare it using the following.

    stadef GtkWidget = GtkWidget_cls

    vtypedef GtkWidget (l:addr) = [c:cls | c <= GtkWidget] gobjref (c, l)

This declares the GtkWidget type to simply be a reference to a glib object (at address l), but it also requires that the object's class be either GtkWidget or a subclass of GtkWidget. Using the hierarchy in this example, this would let you to pass a gobjref with a GtkArrow class to a function that requires a GtkWidget. On the other hand, if a function requires a GtkWidget, and you give it a glib object that is not a subclass of GtkWidget, the type checker will give an error.