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

Google Group
1

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?

2

This one is for building interface for OOP.On Friday, May 15, 2015 at 8:26:42 PM UTC-4, Yannick Duchêne wrote:

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?

3

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.Am Freitag, 15. Mai 2015 20:26:42 UTC-4 schrieb 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?