Doxa Programming Language

Documentation

Doxa is inspired by Nagarjuna's four cornered logic, known as Catuṣkoṭi. Doxa does not use bools but instead a novel logical type called a tetra. A tetra (short for tetralemma) has four possible states or corners:

P (true)
¬ P (false)
P ∧ ¬ P (both)
¬ ( P ∨ ¬ P ) (neither)

Doxa is high level, statically typed, memory managed language. It has a highly readable and consistant syntax aimed at reducing cognative load, and producing code which is simple and aesthetic while remaining type safe. It features an extended logical value called a tetra, as well as a full suite of first order logic operators including existential and universal quantifers.

Usage

Usage:
  doxa run [general options] <file.doxa>
  doxa compile [general options] <file.doxa> -o <output> [compile options]

General options:
  --profile                         # Enable profiling
  --help, -h                        # Show this help message
  --debug-[stage]                   # Enable debug output for [stage]
                                    # lexer, parser, semantic, hir, bytecode, execution
  --debug-verbose                   # Enable all debug output

Compile options:
  -o, --output <path>               # Output executable path (required)
  --arch=<arch>                     # Target CPU architecture (default: host)
  --os=<os>                         # Target operating system (default: host)
  --abi=<abi>                       # Target ABI (optional)
  -O-1 | --opt=-1                   # Debug-aware codegen (peek dumps)
  -O0..-O3 | --opt=0..3             # LLVM and codegen optimization level

Examples:
  doxa run file.doxa
  doxa compile file.doxa -o out/myapp
  doxa compile file.doxa -o out/myapp --arch=x86_64 --os=linux -O2

Building from source

Current build uses Zig 0.15.2, there are no other dependancies.

compile from source and run a file

zig build run -- run ./path/to/file.doxa

for consistent results be sure to build before running compiler tests

zig build
zig build test

Native Types

Doxa is based upon a very small number of types with enums, structs, and type unions providing a huge degree of flexibility to how these core types can be used. Exhaustive match statements and union type narrowing allow for extremly simple yet powerful error handling patterns that takes the idea of errors as values very literally.

Atomic

• int (64-bit integer)
• float (64-bit float)
• byte (8-bit uint hex literal)
• string
• tetra (four-value logic unit)
• nothing (void type)

Molecular

• array (homogeneous)
• struct
• enum
• map
• union

TODO:

• standard lib
• finish the last few internal methods
• zig code blocks

Example

# a brainfuck interpreter implemented in doxa
# mirror-shades

const symbols is [ ">", "<", "+", "-", ".", ",", "[", "]" ]

function getInput() returns byte {
    @print("Input: ")
    var userInput :: string is @input()
    var newByte :: byte is @byte(userInput[0])
    return newByte
}

function startLoop(^loopSpot :: int[], ^loops :: int, ip :: int) {
    if @length(loopSpot) == loops then {
        @push(loopSpot, ip)
    } else {
        loopSpot[loops] is ip
    }
    loops += 1
}

function endLoop(loopSpot :: int[], ^loops :: int, ^ip :: int, tape :: byte[], tp :: int) {
    if loops >= 0 then {
        if tape[tp] == 0 then {
            loops -= 1
        } else {
            const loopPointer is loops - 1
            ip is loopSpot[loopPointer]
            # cancels the ip += 1 from the main loop
            ip -= 1
        }
    }
}

function checkClosingBracket(scan :: string) returns tetra {
    var pointer :: int
    var openBrackets :: int
    while(pointer < @length(scan)) {
        if(scan[pointer] == "[") then openBrackets += 1
        if(scan[pointer] == "]") then openBrackets -= 1
        pointer += 1
        if openBrackets < 0 return false
    }
    return(openBrackets == 0)
}

function interpret(scan :: string) {
    var tape :: byte[10] # increase if needed
    var loops :: int
    var loopSpot :: int[]
    var tp :: int
    var ip :: int

    const scanLength is @length(scan)

    var closedBrackets :: tetra is checkClosingBracket(scan)
    @assert(closedBrackets, "Unmatched brackets")

    while(ip < scanLength) do ip += 1 {
        var currentInstruction is scan[ip]
        if(currentInstruction == ">") then tp += 1
        if(currentInstruction == "<") then tp -= 1
        if(currentInstruction == "+") then tape[tp] += 0x01
        if(currentInstruction == "-") then tape[tp] -= 0x01
        if(currentInstruction == ".") then @print("Output: {tape[tp]}\n")
        if(currentInstruction == ",") then tape[tp] is getInput()
        if(currentInstruction == "[") then startLoop(^loopSpot, ^loops, ip)
        if(currentInstruction == "]") then endLoop(loopSpot, ^loops, ^ip, tape, tp)
    }
}

entry function main() {
    interpret(",+.")
}