XXIIVV

Using stack effect definitions in Uxntal.

The Uxntal notation follows that of the Forth programming language, where each item on the left of the -- spacer is the state of the stack before, and to the right, the state of the stack after:

@routine ( a b -- a b c )
	ADDk
	JMP2r

By default, single items are a byte long, and shorts are indicated with a * suffix, the order in which they appear is the order of the stack with the top item to the right:

@routine ( a b* -- b* a )
	ROT
	JMP2r

In some rare cases, an item is passed to a routine via the return stack, in this case it is prefixed with the ` character indicates items in the return stack to its right. The return address is omitted from the stack effect notation.

@routine ( a* `b* -- )
	POP2 POP2r
	JMP2r

If a specific item on the stack needs to be explicit about it being a pointer that needs to be unquoted, the concatenative notation is written within square brackets.

@routine ( {fn}* -- )
	JMP2

Further notation is available for program verification.

Using program validation in Uxntal.

Type inference in Uxntal is done by checking the stack effect notation of words, against the sum of stack changes predicted to occur based on the items in their bodies.

Words that do not pass the stack-checker are generating a warning, and so essentially this defines a very basic and permissive type system that nevertheless catches some invalid programs and enables compiler optimizations. 

@routine ( a b -: c ) Ok.
	MUL
JMP2r

The simplest case is when a piece of code does not have any branches or recursion, and merely pushes literals and calls words. Pushing a literal has stack effect ( -- x ). The stack effect of most words is always known statically from the declaration.

@add ( a* b* -- c* ) Warning: Imbalance in @add of +2
	DUP2 ADD2
JMP2r

Branch Validation

A word calling a subroutine that would force an exit of the parent routine with an imbalanced stack also triggers an error.

@routine ( a b -: c ) Warning: Imbalance in @routine of +1
	EQUk ?&sub-routine
	POP2 #0a JMP2r
	&sub-routine ( a b -: c* )
		POP2 #000b JMP2r

Return-Stack Passing

The following example shows some extra syntax where stack elements passed through the return stack are separated with a pipe:

@wcpy ( src* des* -: cap* ) Ok.
	STH2
	&w ( src* `des* -: cap* )
		LDAk STH2kr STA
		INC2r INC2 LDAk #20 GTH ?&w
	POP2
	( cap ) #00 STH2kr STA
	INC2r STH2r JMP2r

Each jump label must be defined for a routine's body to validate with the arity checker, but labels can also be used anywhere in a routine to test against a specific arity in time, like you would a breakpoint.

Fall-through Type

The fall-through comment allows to validate a tail-less routine(or, that does not return or break), by including the stack effect of the following routine in memory.

@falling ( a b c -: c ) Ok.
	POP
	( >> )
@next-routine ( a b -: res )
	ADD
JMP2r

More research has to be done in this space, but it would be interesting to check a routine's side-effects by making sure that no ST/LD/DE opcodes can be reached.

Runtime Validation

Lastly, a runtime specific solution to validate the stack state at any one point during the execution of a program, is to read the System/wst port and compare it against a given stack pointer byte value. Note: that the value in the wst and rst ports include the stack pointer byte.

@on-reset ( -> )
	#abcd DUP2 
	.System/wst DEI #05 EQU ?{
		#01 .System/debug DEO
		}
	BRK

incoming uxntal syntax uxntal syntax uxntal types drifblim