Cure

Verification-First Programming

← Back to Documentation

Record Operations Implementation Summary

Overview

This document summarizes the implementation of two new record operations in the Cure programming language:

  1. Direct field access using dot notation: record.field
  2. Record update syntax using pipe notation: Record{base | field: value}

Implementation Date

2025-10-31

Changes Made

1. AST Extensions (src/parser/cure_ast.hrl)

Added two new expression record types:

%% Field access expressions (record.field)
-record(field_access_expr, {
    record,    % Expression evaluating to a record
    field,     % Atom: field name
    location
}).

%% Record update expressions (Record{old | field: value})
-record(record_update_expr, {
    name,      % Record type name
    base,      % Expression for the base record
    fields,    % List of #field_expr{} records
    location
}).

Updated the expr() type definition to include these new types.

2. Parser Enhancements (src/parser/cure_parser.erl)

Field Access Parsing

Record Update Parsing

Helper Functions

3. Type System Integration (src/types/cure_typechecker.erl)

Type Inference for Field Access

infer_expr({field_access_expr, RecordExpr, FieldName, Location}, Env) ->
    % Infer record type, look up field type from record definition
    % Return field type or error if field doesn't exist

Type Inference for Record Update

infer_expr({record_update_expr, RecordName, BaseExpr, Fields, Location}, Env) ->
    % Check base expression matches record type
    % Validate updated fields exist and have correct types
    % Return updated record type

AST Conversion

4. Code Generation (src/codegen/cure_codegen.erl)

Field Access Codegen

compile_record_expr(#field_access_expr{...}, State) ->
    % Generate: maps:get(FieldName, Record)

Record Update Codegen

compile_record_expr(#record_update_expr{...}, State) ->
    % Generate: BaseRecord#{field1 := Value1, field2 := Value2, ...}

Added dispatch cases in compile_expression/2 for the new expression types.

5. BEAM Compiler Integration (src/codegen/curebeamcompiler.erl)

New BEAM Instructions

Record Representation

Changed record compilation from Erlang records to maps:

compile_make_record([RecordName, FieldNames, FieldCount], Context) ->
    % Generate: #{field1 => Val1, field2 => Val2, ...}
    MapForm = {map, Line, MapAssocs}

6. Documentation and Examples

Current State

Note: As of October 31, 2025, the record field access and update operations are fully implemented in the compiler (parser, AST, codegen), but the example files mentioned in earlier documentation do not currently exist. Existing Examples: The current Cure examples that demonstrate record syntax are: Implementation Status:

Syntax Examples

Direct Field Access

def get_name(p: Person): String =
  p.name  # Direct field access

# Chained access
def get_nested_field(contact: Contact): String =
  contact.person.name  # Access nested record fields

Record Update

def birthday(p: Person): Person =
  Person{p | age: p.age + 1}  # Update single field

def move_point(pt: Point, dx: Float, dy: Float): Point =
  Point{pt | x: pt.x + dx, y: pt.y + dy}  # Update multiple fields

Testing

Implementation Verification

✅ Parser Implementation:

✅ Codegen Implementation:

✅ AST Definitions:

Testing Status

Technical Notes

Disambiguation Strategy

The parser disambiguates between module qualification and field access by checking:

  1. If the base expression is a simple identifier (#identifier_expr{})
  2. If there's a ( token after the field name
  3. If both are true → module qualification
  4. Otherwise → field access

Record Update Implementation

The record update syntax is parsed by:

  1. Detecting { after a record type name
  2. Parsing the first expression after {
  3. Checking for | token
  4. If | found → record update, otherwise backtrack to regular construction

BEAM Compilation

Records compile to Erlang maps, which provides:

Future Enhancements

Potential improvements for future iterations:

  1. Nested updates: Person{p | address.city: "New York"}
  2. Pattern-based updates: Person{p | age: a} when a > 18 -> ..}
  3. Partial construction: Allow omitting some fields with defaults
  4. Record spreading: Person{p1 | ...p2} to merge records
  5. Type-safe field access: Compile-time verification of field existence

Compatibility

References

Implementation Files

Example Files