A frustratingly incomplete illustration of what textual relsat code might be like

relsat.rs

//let's break down the highlevel relsat code:

addAndTriple := fn a b ->
	3*(a + b)

//First we'll break down the syntactical sugars until we can see how it translates to a tree
//note that each of these stages are valid rel code, it's all equivalent.

(:= addAndTriple fun( vars(a b) block(
	3*(a + b)
)))

//function calls can name the parameters at the call site, and this is common. + has the signature +(l r)-> o
(:= addAndTriple fun( vars(a b) block(
	(* l:3 r:(+ l:a r:b))
)))

(:= addAndTriple (fun (vars a b) (block
	(* (l 3) (r (+ (l a) (r b))))
)))

//( in other words, it's a tree that has this structure: )
:=
	addAndTriple
	fun
		vars
			a
			b
		block
			*
				l
					3
				r
					+
						l
							a
						r
							b

//(or this:)
:=(addAndTriple fun(vars(a b) block(*(l(3) r(+(l(a) r(b)))))))

//all of these representations will be recognized. relsat is an s-expression based language, however, it has a lot of very robust and transparent syntactical sugars that you should probably use.

//?????? ??? ?????? ???? ? ?????, and, by those means, by simply ??????ing the ?????, we come out with the final result, a sequence of logical relations between entities:

+  l:prog.f0.a  r:prog.f0.b  res:prog.f0.r0
call literalValue  type:Uint32  v:3  into:prog.f0.l0
*  l:prog.f0.r0  r:prog.f0.l0  res:prog.f0.res
equate  prog.f0  prog.addAndTriple
functional  prog.addAndTriple  in(prog.addAndTriple.a  prog.addAndTriple.b)  out(prog.addAndTriple.output)

//when you query res from (prog.addAndTriple  a:2  b:3  output:res), relsat will be able to take the '(functional prog.addAndTriple ...)' rel as a hint that if the inputs to prog.addAndTriple are fully determined (and in this query they are, being literals), the outputs will be fully determined as well, meaning that it can optimize this kind of query into an ordinary function call consisting of a sequence of other ordinary function calls(relsat already knows that + and * are functions as well)

ijr that {Optional naming of parameters at the call site using a pair} isn't viable at all. If you don't distinguish a(a(b)) from a(a:b) ... you're gonna have a bad time