Additional viewer simplification for small instances

[wisnesky]

The reason the viewer doesn’t display the way you’d like is because the elements you want to print nicely are not “definitions in the sense of Patrick”. Here is the type algebra after CQL has simplified it. It contains “definitions” - things that the viewer will simplify - and then the equations, which do not inform the viewer. To obtain this presentation, CQL only applies rewrites of the form

generator -> ...

Usually, this is sufficient because the presentations generated “in bulk” from SQL, CSV, or delta/sigma/pi, will have one labelled null per column in the viewer. Applying rewrites where the LHS is a generator are really fast. In this example, we would need to apply a rewrite (and I’m not even entirely sure name(e) is a definition in Patrick’s sense):

name(e) -> ...

Which although definitely possible is known to slow things down quite a bit. I’ll add a ticket noting this discussion; in the interim, my only suggestion for getting the display you want is the add lots more redundant labelled nulls so that the type algebra simplifier has more rules of the form

generator -> ...

To apply.

functions
    e :  -> G
    m : G, G -> G
    name : G -> String
    inl r : G
    inl f : G
equations
    name(inl f) = sue
    name(((inl f m inl r) m inl r)) = deb
    name(((inl r m inl r) m inl r)) = ryan
    name((inl r m inl r)) = jon
    name((inl f m inl r)) = dave
    (((inl r m inl r) m inl r) m inl r) = e
    name(e) = bob
    name(inl r) = carl
    (inl f m inl f) = e
    (inl f m inl r) = (((inl r m inl f) m inl f) m inl f)
    name((((inl f m inl r) m inl r) m inl r)) = eric

Definitions:
inr (0, posname) -> name(inl f)
inr (1, posname) -> name((inl f m inl r))
inr (0, pos) -> inl f
inr (1, pos) -> (inl f m inl r)

Original Sks:{inr (1, pos), inr (0, pos), inl r, inr (0, posname), inr (1, posname), inl f}

options
    prover = completion
    require_consistency = false

typeside Grp = literal {
    types
        G
        String
    constants
        e:G
        bob sue carl eric ryan deb jon dave : String
    functions
        m: G, G->G
        name: G->String
    equations
        forall g:G. m(g,e)=g
        forall g:G. m(e,g)=g
        forall g1 g2 g3:G. m(m(g1,g2),g3)=m(g1,m(g2,g3))

}

schema Group = literal : Grp {
    entities
        elt
    attributes
        pos: elt->G
        posname: elt->String
    observation_equations
        forall e. name(pos(e))=posname(e)
} 

instance DihedralTypes = literal : Group {
    generators
        f r: G 
    equations
        m(f,f)=e 
        m(m(m(r,r),r),r)=e 
        m(f,r)=m(m(m(r,f),f),f)
        name(e)=bob name(r)=carl    name(m(r,r))=jon    name(m(m(r,r),r))=ryan
        name(f)=sue name(m(f,r))=dave name(m(m(f,r),r))=deb name(m(m(m(f,r),r),r))=eric     

} 

instance myDihedral = literal : Group {
    imports
        DihedralTypes
    generators
        x y:elt
    equations
        x.pos=m(f,r)
        y.pos=f
}