Definition of UampirNexol

This document defines UampirNexol, a typed functional language for machine-language-level program construction.

The definition is illustrated with examples used as test cases.

These tests are written in Falderal format. Each indented code block (generally preceded by a description) represents a test. All the lines of the code block up until the ===> line give the input to be tested; the text after ===> gives the expected output. ???> gives an expected error message, which is permitted to be a partial (substring) match.

Tests for the syntax of UampirNexol can be found in the Syntax of UampirNexol document.

Tests for extraction of 6502 code from UampirNexol expressions can be found in the UampirNexol Extraction document.

Evaluation

Although UampirNexol is not designed for direct evaluation, it is important that we have a definition of the meaning of each function, so that we can reason about it formally. These definitions give us the ability to evaluate a UampirNexol expression.

-> Tests for functionality "Evaluate UampirNexol Expression"

-> Functionality "Evaluate UampirNexol Expression" is implemented by
-> shell command "bin/uampirnexol run %(test-body-file)"

Basic straight-line code.

LDA# 0xff ; TAX ; INX
===> State {contents = fromList [(A,255),(X,0),(Z,1),(N,0)]}

Conditional.

LDA# 0 ; if Z INX else INY
===> State {contents = fromList [(A,0),(X,1),(Z,0),(N,0)]}

LDA# 1 ; if Z INX else INY
===> State {contents = fromList [(A,1),(Y,1),(Z,0),(N,0)]}

let block.

let
    value = 20
in
    LDA# value ; if Z INX else INY
===> State {contents = fromList [(A,20),(Y,1),(Z,0),(N,0)]}

Call routine.

let
    bumpupx = routine (INX; INX; INX)
in
    LDA# 40 ; TAX ; (call bumpupx) ; (call bumpupx) ; INX
===> State {contents = fromList [(A,40),(X,47),(Z,0),(N,0)]}

Type Assignment

-> Tests for functionality "Assign Type to UampirNexol Expression"

-> Functionality "Assign Type to UampirNexol Expression" is implemented by
-> shell command "bin/uampirnexol type %(test-body-file)"

Instructions have a function type mapping machine states to machine states, but each of those states has a more detailed type that specifies which locations are meaningful and which are unmeaningful.

INX
===> (State[X/] -> State[X,Z,N/])

; is syntax for a higher-order function that composes two functions.

INX ; INX
===> (State[X/] -> State[X,Z,N/])

INX ; INY
===> (State[X,Y/] -> State[X,Y,Z,N/])

The type of literal integers.

123
===> Byte

LDA# is a higher-order function, and this is its type.

LDA#
===> (Byte -> (State[/] -> State[A,Z,N/]))

LDA# can be applied to a byte to yield a first-order function.

LDA# 0
===> (State[/] -> State[A,Z,N/])

LDA# cannot be applied to a non-byte.

LDA# INX
???> error: Unacceptable argument type

STA is a higher-order function, and this is its type. FIXME: its type actually looks more like a dependent type in this context; the location it takes is part of its output type. But we haven't captured that here yet. When we implement a more general typing scheme, the output type of the function should look something like State[*1/] where *1 indicates the location which is the 1st argument to the preceding function. Or smth.

STA
===> (Loc -> (State[A/] -> State[/]))

STA can be applied to an address location to yield a first-order function.

STA @1024
===> (State[A/] -> State[Address 1024/])

STA cannot be applied to a non-location.

STA 1024
???> error: Unacceptable argument type

STA cannot be applied to a non-address location.

STA C
???> error: STA must be applied to a known address location

Here is the type of TAX. A needs to be meaningful on its input, so it appears in the meaningful set of the input state type. But the instruction does not change A, so it does not appear in the meaningful set of the output state type. It does not appear in the unmeaningful set either - which indicates it is untouched (its value is preserved).

TAX
===> (State[A/] -> State[X,Z,N/])

When LDA# 0 is composed with TAX though, the A that TAX needs to be meaningful on its input is supplied by LDA# 0's output; and the A that was supplied as meaningful on LDA# 0's output, is also supplied as meaningful on the composition.

LDA# 0 ; TAX
===> (State[/] -> State[A,X,Z,N/])

Type of a conditional.

if C TAX else TAX
===> (State[A,C/] -> State[X,Z,N/])

Even if a location is a required input in only one branch, it's a required input for the whole if expression. Also for outputs.

if C CLC else INX
===> (State[X,C/] -> State[X,Z,C,N/])

Type of a repeat loop. Note how Z is not required to be defined on input to the loop (because it is not set until after the body has executed).

repeat INX until Z
===> (State[X/] -> State[X,Z,N/])

But on the other hand, if the flag being tested is not set by the body, it is required on input. (Note that this could also be used by an implementation to warn that the loop is vacuous!)

repeat INX until C
===> (State[X,C/] -> State[X,Z,N/])

Type of a while loop. Note how, in this case, Z is required to be defined on input to the loop.

while ~Z do INX
===> (State[X,Z/] -> State[X,Z,N/])

Type of a let block is the type of its body.

let foo = 0 in (LDA# foo ; TAX)
===> (State[/] -> State[A,X,Z,N/])

But of course the value being bound must type-check.

let foo = LDA# INX in (LDA# foo ; TAX)
???> error: Unacceptable argument type

And the type of the variable once bound must type-check in its usage.

let foo = INX in (LDA# foo ; TAX)
???> error: Unacceptable argument type

Routines

Type of routines.

routine (LDA# 0; TAX)
===> Routine(State[/] -> State[A,X,Z,N/])

call routine (LDA# 0; TAX)
===> (State[/] -> State[A,X,Z,N/])

Trashing

The trash directive declares the value in a location to be unmeaningful. Trying to use that value is a type error.

trash A
===> (State[/] -> State[/A])

(trash A) ; (trash A)
===> (State[/] -> State[/A])

(trash A) ; (trash X)
===> (State[/] -> State[/A,X])

TAX ; TAX
===> (State[A/] -> State[X,Z,N/])

TAX ; TAX ; (trash A)
===> (State[A/] -> State[X,Z,N/A])

TAX ; (trash A) ; TAX
???> Locations expected to be meaningful: A

TAX ; (trash X) ; TAX
===> (State[A/] -> State[X,Z,N/])

Routines can trash locations too.

let
    foo = routine (TAX ; (trash X))
in
    call foo
===> (State[A/] -> State[Z,N/X])

extern

An extern represents a routine that is defined elsewhere. The UampirNexol program takes it on faith that the routine exists. To this end, the extern declaration includes a type declaration.

extern @0xffd2 : State[A/] -> State[A/]
===> Routine(State[A/] -> State[A/])

Calling an extern is like calling a defined routine.

let
    chrout = extern @0xffd2 : State[A/] -> State[A/]
in
    call chrout
===> (State[A/] -> State[A/])

Often, extern routines are declared to trash one or more locations.

extern @0xffd2 : State[A/] -> State[ /A]
===> Routine(State[A/] -> State[/A])

let
    chrout = extern @0xffd2 : State[A/] -> State[ /A]
in
    LDA# 40
===> (State[/] -> State[A,Z,N/])

let
    chrout = extern @0xffd2 : State[A/] -> State[/A]
in
    call chrout
===> (State[A/] -> State[/A])

let
    chrout = extern @0xffd2 : State[A/] -> State[/A]
in
    LDA# 40 ; (call chrout)
===> (State[/] -> State[Z,N/A])