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
}