What DEXA actually supports right now

Types

Types implemented in the typechecker and interpreter:

• int — 64-bit signed integer.
• float — 64-bit floating point.
• bool — true / false.
• string — immutable UTF-8 string.
• unit — no value / void; implicit when a function doesn’t declare a return type.
• address — a distinct, concrete address/identity type.
• Record<Name> — nominal record types introduced by model and contract.

There are no implicit coercions in DEXA. In particular, there is no implicit string ↔ address. Conversions must be explicit via the address("...") builtin.

Nominal records (models & contracts)

Nominal record types are declared via model or contract. Records are nominal: two record types with identical fields are still different types.

model Wallet {
    owner: address
    balance: int
}

• Field types are checked: assigning the wrong type to a field is a compile-time error.
• Records exist at runtime as Value::Record with a nominal type_name and fields.
• Records are printable via Display, e.g. Wallet{owner=addr:debug, balance=3}.

Record literals

let w: Wallet = Wallet { owner: address("addr:test"); balance: 0; };

• Field order is not significant.
• Duplicate fields are a compile error.
• Unknown fields are a compile error.
• For literals without a base record, lowering produces a fully materialized record (all declared fields present).

Defaults & record update

• Defaults are applied during lowering for record literals without a base; the runtime does not inject defaults.
• Record update syntax exists: Type { ..base; field: expr; ... }.
• base must be the same nominal record type as Type (typecheck error on mismatch).
• Updates may remain in IR and are merged by the interpreter at runtime.

Functions

Declared with fn:

fn add(a: int, b: int) -> int {
    return a + b;
}

• Parameters must have explicit types.
• Return type can be omitted; defaults to unit.
• Calls are type-checked for arity and parameter types.

Variables & mutability

fn main() -> int {
    let x: int = 1;        // immutable
    let mut y: int = 2;    // mutable

    // x = 3;   // ❌ compile-time error
    y = y + 1; // ✅

    return y;
}

• let creates an immutable binding.
• let mut creates a mutable binding.
• Assignments are checked: you can’t write to non-mut variables.
• Explicit type annotations are required for now (type inference will be a later feature).

Expressions & operators

Currently implemented expression forms:

• Literals: ints, floats, strings, bools.
• Identifiers referring to local variables or parameters.
• Binary arithmetic: + - * / (type-checked numeric operands).
• Comparisons: <, <=, >, >=, ==, != → bool.
• Logical: &&, || on bool.
• Function calls with positional arguments.

fn main() -> bool {
    let x: int = 10;
    let y: int = 20;
    let bigger: int = max(x, y);
    return bigger > 15 && bigger < 30;
}

Control flow

Implemented constructs

• if / else with a boolean condition.
• Nested blocks with scoped variables and shadowing.
• return with or without value.
• while <cond> { ... } — pre-conditioned loops.
• loop { ... } — infinite loops controlled with break.
• break — exits the innermost while / loop.
• continue — jumps to the next iteration of the innermost loop.

fn classify(x: int) -> bool {
    if x >= 0 && x < 10 {
        return true;
    } else {
        return false;
    }
}

fn countdown(start: int) {
    let mut x: int = start;

    while x > 0 {
        x = x - 1;
        if x == 2 {
            continue;
        }
        if x == 1 {
            break;
        }
    }

    return;
}

Builtins / special forms

Implemented builtins / special forms:

• print(expr) — appends rendered output to prints (the interpreter does not write to stdout).
• address(string) -> address — explicit conversion; required for address defaults and address-typed fields.
• require(cond, msg?) — typed check and controlled abort semantics.

require

fn main() {
    let x: int = 5;
    require(x > 0);
    require(x > 0, "x must be positive");
    return;
}

• First argument must be bool, enforced by the typechecker.
• On failure, execution aborts and the interpreter returns ProgramResult::RequireFail (not a panic).
• The returned failure includes the message plus the accumulated trace and gas.

Execution model (current prototype)

The reference compiler currently targets a simple interpreted IR. Every DEXA program goes through:

1. Parse source into an AST (functions, blocks, if/else, expressions).
2. Typecheck with an explicit environment of locals, function signatures, and nominal record types.
3. Lower to a small IR with locals, basic blocks, If, While, Loop, Return, calls, and records.
4. Validate IR invariants (fail-fast firewall) before execution.
5. Interpret the IR to produce a structured program result rather than just a raw integer.

Executing main always yields a ProgramResult:

ProgramResult::Ok {
    value: Value,
    prints: Vec<String>,
    trace: ExecutionTrace,
    gas: GasMeter,
}

ProgramResult::RequireFail {
    message: String,
    trace: ExecutionTrace,
    gas: GasMeter,
}

• value — the final return value of main (int, bool, record, unit, etc.).
• prints — every print(...) call in order.
• trace — a function-level execution trace (main → ...).
• gas — a deterministic step counter (function entries + statements + expressions).

IR validation exists to stop the runtime from “accepting garbage.” For records, this includes invariants like: known record types, no duplicate fields, no unknown fields, and fully materialized record literals after lowering.