cure

v0.1.0

Cure Programming Language

A strongly-typed, dependently-typed programming language for the BEAM virtual machine with built-in finite state machines, complete import system, and comprehensive standard library.

🚀 Last Updated: October 31, 2025

✅ Working import system with full module resolution
✅ Standard library with verified runtime execution (12 modules)
✅ Dependent types with compile-time verification
✅ Complete compiler pipeline from source to BEAM bytecode
✅ FSM runtime system with native BEAM integration
✅ Type-directed optimizations (25-60% performance improvement)
✅ Comprehensive testing infrastructure with high success rate
✅ LSP Server with real-time diagnostics and IDE integration
✅ SMT Solver Integration (API level - CLI integration planned)
✅ Guard Compilation with runtime validation and optimization
✅ Record operations with field access and update syntax

Core Features

✅ Production-Ready Components

🚀 Complete Import System: Full module resolution with import Module [functions] syntax

📚 Working Standard Library: 12 modules (core, io, show, list, fsm, result, pair, vector, string, math, system, rec) with essential functions

🎯 Dependent Types: Length-indexed vectors, refinement types with internal constraint representation

🎆 Finite State Machines: Arrow-based transition syntax (State1 --> |event| State2) compiling to BEAM behaviors

⚡ Type-Directed Optimizations: Monomorphization, function specialization, inlining (25-60% improvement)

🏗️ BEAM Integration: Native compilation to BEAM bytecode with OTP compatibility

🔧 Pattern Matching: Match expressions with guards and dependent type constraints

📊 Complete Testing Infrastructure: Comprehensive test suites covering all compiler stages

🔌 LSP Server: Language Server Protocol implementation with real-time diagnostics and hover info

⚙️ Guard Compilation: Dependent type guard validation with runtime optimization

🧮 SMT Integration: Z3/CVC5 solver integration at API level (CLI integration planned)

📝 Record Operations: Field access (record.field) and update syntax (Record{base | field: value})

🎯 Language Capabilities

Control Flow: Match expressions with pattern guards (note: if-then-else not implemented)

String Operations: Concatenation with <> operator, charlist literals with Unicode curly quotes

List Operations: Cons operator | for pattern matching [h | t]

SMT-Based Constraint Solving: Z3/CVC5 integration at API level for type constraints

Error Handling: Result/Option types from standard library

CLI & Build System: Complete development toolchain with wrapper scripts

IDE Integration: LSP server with real-time diagnostics and hover information

Enhanced Error Messages: Precise location tracking with source code snippets

📋 Planned Features (See TODO.md for details)

Pipe Operator: |> for function chaining (parser support exists, needs verification)

Type Classes/Traits: Polymorphic interfaces with typeclass and instance keywords

If-Then-Else: Traditional conditional expressions

String Interpolation: Template-based string construction

Advanced FSM Syntax: Guards and actions in state transitions

Effect System: Computational effects tracking

Macro System: Compile-time code generation

Project Structure

cure/
├── src/
│   ├── lexer/          # Tokenization and lexical analysis
│   ├── parser/         # Syntax analysis, AST generation, and error reporting
│   ├── types/          # Dependent type system implementation
│   ├── codegen/        # BEAM bytecode generation and guard compilation
│   ├── fsm/            # Finite state machine primitives
│   ├── smt/            # SMT solver integration (Z3, CVC5)
│   ├── lsp/            # Language Server Protocol implementation
│   └── runtime/        # Runtime system integration
├── lib/                # Standard library
├── test/               # Comprehensive test suites
├── examples/           # Example programs
└── docs/              # Language specification and documentation

Getting Started

Quick Start

# Build the compiler
make all

# Try the FSM traffic light example
./cure examples/06_fsm_traffic_light.cure

# Run the compiled program
erl -pa _build/ebin -noshell -eval "'TrafficLightDemo':main(), init:stop()."

# Expected output:
# Starting traffic light FSM...
# Current state: red
# [Traffic light transitions through states]

# Show help
./cure --help

# Run test suite
make test

Installation

Prerequisites: Erlang/OTP 20+, Make, Unix-like environment

# Clone and build
git clone <repository>
cd cure
make all

# Verify installation
./cure --version

# Run tests
make test

Command Line Interface

The Cure compiler includes a comprehensive CLI for compiling .cure files to BEAM bytecode.

Basic usage:

cure [OPTIONS] <input-file>

Key options:

-o, --output <file>: Specify output file

-d, --output-dir <dir>: Set output directory

--verbose: Enable detailed output

--no-type-check: Skip type checking

See docs/CLI_USAGE.md for complete documentation.

Language Examples

List Processing with Standard Library

module ListDemo do
  export [demo/0]

  import Std.List [map, filter, fold]
  import Std.IO [print]

  def demo(): Unit =
    let numbers = [1, 2, 3, 4, 5]

    # Map operation
    let doubled = map(numbers, fn(x) -> x * 2 end)
    print("Doubled: " <> show(doubled))

    # Filter operation
    let evens = filter(numbers, fn(x) -> x % 2 == 0 end)
    print("Evens: " <> show(evens))

    # Fold operation
    let sum = fold(numbers, 0, fn(x, acc) -> acc + x end)
    print("Sum: " <> show(sum))
end

Result Type Error Handling

module ResultDemo do
  export [safe_divide/2]

  import Std.Result [ok, error, map, and_then]

  def safe_divide(a: Int, b: Int): Result(Int, String) =
    match b do
      0 -> error("Division by zero")
      _ -> ok(a / b)
    end

  def compute(): Result(Int, String) =
    and_then(safe_divide(10, 2), fn(x) ->
      map(safe_divide(x, 0), fn(y) -> y * 2 end)
    end)
end

Pattern Matching with Guards

module Guards do
  export [classify/1]

  def classify(x: Int): Atom =
    match x do
      n when n < 0 -> :negative
      0 -> :zero
      n when n > 0 -> :positive
    end
end

Finite State Machine (Arrow-Based Syntax)

module TrafficLight do
  export [create/0, next/1]

  import Std.FSM [fsm_new, fsm_send, fsm_stop]
  import Std.Pair [pair]

  # Define FSM with arrow-based transitions
  fsm TrafficLight do
    initial: :red

    :red --> |:timer| :green
    :green --> |:timer| :yellow
    :yellow --> |:timer| :red

    :green --> |:emergency| :red
  end

  def create(): FSM(TrafficLight) =
    fsm_new(TrafficLight, :red)

  def next(fsm: FSM(TrafficLight)): FSM(TrafficLight) =
    fsm_send(fsm, pair(:timer, unit()))
end

Record Operations

module Records do
  export [demo/0]

  record Person do
    name: String
    age: Int
    email: String
  end

  def demo(): Unit =
    let person = Person{name: "Alice", age: 30, email: "alice@example.com"}

    # Field access
    let name = person.name

    # Record update (immutable)
    let older = Person{person | age: 31}

    print("Name: " <> name)
    print("New age: " <> show(older.age))
end

Available Examples

See the examples/ directory for working code:

01_list_basics.cure - List operations and standard library functions

02_result_handling.cure - Error handling with Result type

03_option_type.cure - Optional values with Option type

04_pattern_guards.cure - Pattern matching with guard clauses

05_recursion.cure - Recursive functions and tail call optimization

06_fsm_traffic_light.cure - Complete FSM implementation

Implementation Status

✅ Complete & Functional (~85% Core Features)

Lexical Analysis: Complete tokenizer with position tracking and error recovery

Parsing: Full AST generation with recursive descent parsing and comprehensive error handling

Type System: Dependent type checking with refinement types (internal constraint representation)

Type Optimization: Monomorphization, specialization, inlining, dead code elimination (25-60% performance gain)

FSM System: Arrow-based FSM syntax compiling to BEAM behaviors with runtime operations

Code Generation: BEAM bytecode generation with debug information and OTP compatibility

Standard Library: 12 working modules (core, io, show, list, fsm, result, pair, vector, string, math, system, rec)

Record Operations: Field access and update syntax fully implemented

Pattern Matching: Match expressions with guards and dependent type constraints

CLI & Build System: Complete development toolchain with wrapper scripts

Testing Infrastructure: Comprehensive test suites covering lexer, parser, types, FSM, codegen

LSP Server: Language server with real-time diagnostics and hover information

SMT Integration: Z3/CVC5 solver integration at API level

📋 Missing Critical Features (~15% - See TODO.md)

Pipe Operator: |> for function chaining (parser recognizes, needs implementation verification)

Type Classes/Traits: Polymorphic interfaces with typeclass/instance keywords not recognized

If-Then-Else: Traditional conditional expressions (currently only match expressions)

String Interpolation: Template-based string construction (AST exists, implementation unclear)

Advanced FSM Syntax: Guards and actions in state transitions

CLI SMT Integration: Command-line options for SMT solver (API works, CLI planned)

🏗️ Future Features (Research/Experimental)

Effect System: Computational effects tracking and management

Macro System: Compile-time code generation and metaprogramming

Linear Types: Resource management and memory safety

Gradual Typing: Mixed static/dynamic typing for Erlang interoperability

Distributed FSMs: Cross-node state machine coordination

Package Manager: Dependency management and distribution

Performance Characteristics

Compilation Performance

Small files (<100 lines): <1 second

Medium projects (1K-10K lines): 5-30 seconds

Large projects (100K+ lines): 30-300 seconds with incremental compilation

Runtime Performance

Function calls: ~10ns overhead (after type-directed optimization)

FSM events: ~1μs including message passing

Type checking: Zero runtime overhead (compile-time only)

Memory usage: Comparable to equivalent Erlang code

Optimization impact: 25-60% performance improvement over unoptimized code

Documentation

Comprehensive documentation is available in the docs/ directory:

LANGUAGE_SPEC.md - Complete language specification

TYPE_SYSTEM.md - Dependent types and type system details

FSM_USAGE.md - Finite state machine guide

FEATURE_REFERENCE.md - Quick reference for all language features

STD_SUMMARY.md - Standard library module documentation

TODO.md - Missing features and future work

EDITOR_SETUP.md - IDE configuration for Cure development

Community & Development

Cure is a research and educational project demonstrating advanced programming language concepts in a practical, BEAM-compatible implementation.

Contributing

Contributions welcome! Priority areas (see TODO.md):

Pipe operator implementation - Complete |> integration

Type classes/traits - Polymorphic interface system

If-then-else expressions - Traditional control flow

Standard library expansion - More utility functions

String interpolation - Template-based strings

Developer tooling - Enhanced IDE support

Documentation and examples - More learning resources

License

To be determined based on project direction and community needs.

cure_action_compiler

Summary

Functions

analyze_action_safety(Action, State)

compile_action(Action, State)

compile_actions(Actions, State)

is_action_safe(_)

optimize_action(Action)

Functions

analyze_action_safety(Action, State)

compile_action(Action, State)

compile_actions(Actions, State)

is_action_safe(_)

optimize_action(Action)

cure_ast

Cure Programming Language - AST Definitions

This module defines the Abstract Syntax Tree (AST) node types and structure for the Cure programming language. It provides comprehensive type definitions and helper functions for creating and manipulating AST nodes throughout the compilation pipeline.

Overview

The Cure AST represents the complete syntactic structure of Cure programs including:

Programs: Collections of top-level items

Modules: Module definitions with exports and items

Functions: Function definitions with parameters, return types, and bodies

Types: User-defined types, primitives, and complex type expressions

FSMs: Finite state machine definitions with states and transitions

Expressions: All forms of expressions (literals, function calls, control flow)

Patterns: Pattern matching constructs

Location Information: Source position tracking for error reporting

AST Structure

Top-Level Items

Programs consist of top-level items:

module_def() - Module definitions

function_def() - Regular function definitions

erlang_function_def() - Erlang interop functions

type_def() - User-defined type definitions

fsm_def() - Finite state machine definitions

import_def() - Import statements

Expression Types

Expressions represent computations and values:

literal_expr() - Literals (numbers, strings, atoms)

identifier_expr() - Variable and function names

function_call_expr() - Function calls with arguments

binary_op_expr() - Binary operations (+, -, *, etc.)

unary_op_expr() - Unary operations (-, not)

match_expr() - Pattern matching expressions

let_expr() - Let bindings

list_expr() - List literals

tuple_expr() - Tuple literals

record_expr() - Record construction

lambda_expr() - Anonymous functions

Type System

Type expressions represent Cure's type system:

primitive_type() - Built-in types (Int, String, Bool, etc.)

dependent_type() - Parameterized types with dependencies

function_type() - Function type signatures

union_type() - Union types (T | U)

list_type() - List types

tuple_type() - Tuple types

type_param() - Type parameters for generics

Pattern Matching

Patterns for destructuring and matching:

wildcard_pattern() - Wildcard patterns (_)

literal_pattern() - Literal value patterns

identifier_pattern() - Variable binding patterns

list_pattern() - List destructuring patterns

tuple_pattern() - Tuple destructuring patterns

record_pattern() - Record field patterns

constructor_pattern() - Constructor patterns (Ok(x), Error(e))

FSM Support

First-class finite state machine support:

fsm_def() - FSM type definitions

state_def() - Individual state definitions

transition() - State transitions with events, guards, and actions

Location Tracking

All AST nodes include location information for:

Error Reporting: Precise source locations for compilation errors

Debugging: Source mapping for runtime errors

IDE Support: Language server integration

Documentation: API documentation generation

Usage Example

%% Create a simple function definition
Params = [#param{name = x, type = int_type(), location = Location}],
Body = #literal_expr{value = 42, location = Location},
Function = cure_ast:new_function(identity, Params, int_type(), undefined, Body).

%% Create an FSM definition
States = [idle, running, stopped],
Initial = idle,
StateDefs = [IdleState, RunningState, StoppedState],
FSM = cure_ast:new_fsm(state_machine, States, Initial, StateDefs).

Design Principles

Immutability

AST nodes are immutable records that can be safely shared and transformed without side effects.

Composability

Complex AST structures are built by composing simpler nodes, enabling modular construction and transformation.

Location Preservation

Every AST node maintains source location information to support high-quality error messages and debugging.

Type Safety

Erlang type specifications ensure AST node integrity and enable static analysis tools to verify AST manipulation code.

Integration

This module integrates with:

Parser: Produces AST nodes from token streams

Type Checker: Analyzes and annotates AST with type information

Compiler: Transforms AST through various compilation phases

Error Reporter: Uses location information for error messages

Performance Considerations

Memory Efficient: Records are lightweight with minimal overhead

Copy-on-Write: Erlang's immutable data structures optimize memory usage

Pattern Matching: Efficient pattern matching on AST node types

Location Sharing: Location records can be shared between related nodes

Summary

Types

binary_op_expr()

binding()

dependent_type()

erlang_function_def()

export_spec()

expr()

field_expr()

field_pattern()

fsm_def()

function_call_expr()

function_def()

function_type()

identifier_expr()

identifier_pattern()

import_def()

item()

lambda_expr()

let_expr()

list_expr()

list_pattern()

list_type()

literal_expr()

literal_pattern()

location()

match_clause()

match_expr()

module_def()

param()

pattern()

primitive_type()

program()

record_expr()

record_pattern()

state_def()

transition()

tuple_expr()

tuple_pattern()

tuple_type()

type_def()

type_expr()

type_param()

unary_op_expr()

union_type()

wildcard_pattern()

Functions

new_expr/3

Creates a new expression AST node with location information.

new_fsm(Name, States, Initial, StateDefs, Location)

Creates a new FSM definition AST node.

new_function(Name, Params, ReturnType, Constraint, Body, Location)

Creates a new function definition AST node.

new_module(Name, Exports, Items, Location)

Creates a new module definition AST node.

new_type_def(Name, Params, Definition, Location)

Creates a new type definition AST node.

Types

binary_op_expr()

-type binary_op_expr() ::
          #binary_op_expr{op :: atom(), left :: expr(), right :: expr(), location :: location()}.

binding()

-type binding() :: #binding{pattern :: pattern(), value :: expr(), location :: location()}.

dependent_type()

-type dependent_type() ::
          #dependent_type{name :: atom(), params :: [type_param()], location :: location()}.

erlang_function_def()

-type erlang_function_def() ::
          #erlang_function_def{name :: atom(),
                               params :: [param()],
                               return_type :: type_expr(),
                               constraint :: expr() | undefined,
                               erlang_body :: string(),
                               location :: location()}.

export_spec()

-type export_spec() :: #export_spec{name :: atom(), arity :: integer(), location :: location()}.

expr()

-type expr() ::
          literal_expr() |
          identifier_expr() |
          function_call_expr() |
          match_expr() |
          let_expr() |
          binary_op_expr() |
          unary_op_expr() |
          list_expr() |
          tuple_expr() |
          record_expr() |
          lambda_expr().

field_expr()

-type field_expr() :: #field_expr{name :: atom(), value :: expr(), location :: location()}.

field_pattern()

-type field_pattern() :: #field_pattern{name :: atom(), pattern :: pattern(), location :: location()}.

fsm_def()

-type fsm_def() ::
          #fsm_def{name :: atom(),
                   states :: [atom()],
                   initial :: atom(),
                   state_defs :: [state_def()],
                   location :: location()}.

function_call_expr()

-type function_call_expr() ::
          #function_call_expr{function :: expr(), args :: [expr()], location :: location()}.

function_def()

-type function_def() ::
          #function_def{name :: atom(),
                        params :: [param()],
                        return_type :: type_expr() | undefined,
                        constraint :: expr() | undefined,
                        body :: expr(),
                        location :: location()}.

function_type()

-type function_type() ::
          #function_type{params :: [type_expr()], return_type :: type_expr(), location :: location()}.

identifier_expr()

-type identifier_expr() :: #identifier_expr{name :: atom(), location :: location()}.

identifier_pattern()

-type identifier_pattern() :: #identifier_pattern{name :: atom(), location :: location()}.

import_def()

-type import_def() :: #import_def{module :: atom(), items :: [atom()] | all, location :: location()}.

item()

-type item() ::
          module_def() | function_def() | erlang_function_def() | type_def() | fsm_def() | import_def().

lambda_expr()

-type lambda_expr() :: #lambda_expr{params :: [param()], body :: expr(), location :: location()}.

let_expr()

-type let_expr() :: #let_expr{bindings :: [binding()], body :: expr(), location :: location()}.

list_expr()

-type list_expr() :: #list_expr{elements :: [expr()], location :: location()}.

list_pattern()

-type list_pattern() ::
          #list_pattern{elements :: [pattern()], tail :: pattern() | undefined, location :: location()}.

list_type()

-type list_type() ::
          #list_type{element_type :: type_expr(), length :: expr() | undefined, location :: location()}.

literal_expr()

-type literal_expr() :: #literal_expr{value :: term(), location :: location()}.

literal_pattern()

-type literal_pattern() :: #literal_pattern{value :: term(), location :: location()}.

location()

-type location() :: #location{line :: integer(), column :: integer(), file :: string() | undefined}.

match_clause()

-type match_clause() ::
          #match_clause{pattern :: pattern(),
                        guard :: expr() | undefined,
                        body :: expr(),
                        location :: location()}.

match_expr()

-type match_expr() :: #match_expr{expr :: expr(), patterns :: [match_clause()], location :: location()}.

module_def()

-type module_def() ::
          #module_def{name :: atom(),
                      exports :: [export_spec()],
                      items :: [item()],
                      location :: location()}.

param()

-type param() :: #param{name :: atom(), type :: type_expr(), location :: location()}.

pattern()

-type pattern() ::
          wildcard_pattern() |
          literal_pattern() |
          identifier_pattern() |
          list_pattern() |
          tuple_pattern() |
          record_pattern().

primitive_type()

-type primitive_type() :: #primitive_type{name :: atom(), location :: location()}.

program()

-type program() :: [item()].

record_expr()

-type record_expr() :: #record_expr{name :: atom(), fields :: [field_expr()], location :: location()}.

record_pattern()

-type record_pattern() ::
          #record_pattern{name :: atom(), fields :: [field_pattern()], location :: location()}.

state_def()

-type state_def() :: #state_def{name :: atom(), transitions :: [transition()], location :: location()}.

transition()

-type transition() ::
          #transition{event :: expr(),
                      guard :: expr() | undefined,
                      target :: atom(),
                      action :: expr() | undefined,
                      location :: location()}.

tuple_expr()

-type tuple_expr() :: #tuple_expr{elements :: [expr()], location :: location()}.

tuple_pattern()

-type tuple_pattern() :: #tuple_pattern{elements :: [pattern()], location :: location()}.

tuple_type()

-type tuple_type() :: #tuple_type{element_types :: [type_expr()], location :: location()}.

type_def()

-type type_def() ::
          #type_def{name :: atom(),
                    params :: [atom()],
                    definition :: type_expr(),
                    location :: location()}.

type_expr()

-type type_expr() ::
          primitive_type() |
          dependent_type() |
          function_type() |
          union_type() |
          list_type() |
          tuple_type().

type_param()

-type type_param() ::
          #type_param{name :: atom() | undefined, value :: type_expr() | expr(), location :: location()}.

unary_op_expr()

-type unary_op_expr() :: #unary_op_expr{op :: atom(), operand :: expr(), location :: location()}.

union_type()

-type union_type() :: #union_type{types :: [type_expr()], location :: location()}.

wildcard_pattern()

-type wildcard_pattern() :: #wildcard_pattern{location :: location()}.

Functions

new_expr/3

-spec new_expr(atom(), term(), location()) -> expr().

Creates a new expression AST node with location information.

Arguments

Type - Expression type (literal, identifier, etc.)

Data - Expression data appropriate for the type

Location - Source location information

Returns

expr() - Expression AST node

error({unknown_expr_type, Type, Data, Location}) - Unknown expression type

Supported Types

literal - Creates a literal expression from the value

identifier - Creates an identifier expression from the name

Example

Literal = cure_ast:new_expr(literal, 42, Location),
Identifier = cure_ast:new_expr(identifier, variable_name, Location).

Note

This is a limited helper function that only supports basic expression types. For complex expressions, construct the records directly.

new_fsm(Name, States, Initial, StateDefs, Location)

-spec new_fsm(atom(), [atom()], atom(), [state_def()], location()) -> fsm_def().

Creates a new FSM definition AST node.

Arguments

Name - FSM name (atom)

States - List of state names

Initial - Initial state name

StateDefs - List of state definitions with transitions

Location - Source location information

Returns

fsm_def() - FSM definition AST node

Example

States = [idle, running, stopped],
StateDefs = [IdleState, RunningState, StoppedState],
FSM = cure_ast:new_fsm(counter, States, idle, StateDefs, Location).

new_function(Name, Params, ReturnType, Constraint, Body, Location)

-spec new_function(atom(), [param()], type_expr() | undefined, expr() | undefined, expr(), location()) ->
                      function_def().

Creates a new function definition AST node.

Arguments

Name - Function name (atom)

Params - List of function parameters

ReturnType - Return type expression (undefined if not specified)

Constraint - Optional constraint expression for the function

Body - Function body expression

Location - Source location information

Returns

function_def() - Function definition AST node

Example

Params = [#param{name = x, type = IntType, location = Loc}],
Body = #literal_expr{value = 42, location = Loc},
Function = cure_ast:new_function(identity, Params, IntType, undefined, Body, Location).

new_module(Name, Exports, Items, Location)

-spec new_module(atom(), [export_spec()], [item()], location()) -> module_def().

Creates a new module definition AST node.

Arguments

Name - Module name (atom)

Exports - List of export specifications

Items - List of top-level items in the module

Location - Source location information

Returns

module_def() - Module definition AST node

Example

Exports = [#export_spec{name = hello, arity = 1, location = Loc}],
Items = [FunctionDef],
Module = cure_ast:new_module('MyModule', Exports, Items, Location).

new_type_def(Name, Params, Definition, Location)

-spec new_type_def(atom(), [atom()], type_expr(), location()) -> type_def().

Creates a new type definition AST node.

Arguments

Name - Type name (atom)

Params - List of type parameter names

Definition - Type expression defining the type

Location - Source location information

Returns

type_def() - Type definition AST node

Example

Params = [t],
Definition = #union_type{types = [IntType, StringType], location = Loc},
TypeDef = cure_ast:new_type_def('Maybe', Params, Definition, Location).

cure_beam_compiler

Summary

Functions

compile_function_to_erlang(_, StartLine)

compile_function_to_erlang(_, StartLine, ModuleName, LocalFunctions)

compile_function_to_erlang(_, StartLine, ModuleName, LocalFunctions, ImportedFunctions)

compile_instructions_to_forms(Instructions, Context)

optimize_instructions(Instructions)

validate_erlang_forms(Forms)

Functions

compile_function_to_erlang(_, StartLine)

compile_function_to_erlang(_, StartLine, ModuleName, LocalFunctions)

compile_function_to_erlang(_, StartLine, ModuleName, LocalFunctions, ImportedFunctions)

compile_instructions_to_forms(Instructions, Context)

optimize_instructions(Instructions)

validate_erlang_forms(Forms)

cure_cli

Cure Programming Language - Command Line Interface

This module provides a comprehensive command-line interface for the Cure programming language compiler. It handles argument parsing, file compilation, and the complete compilation pipeline from Cure source code to BEAM bytecode.

Features

Complete CLI Interface: Argument parsing with support for all compiler options

Full Compilation Pipeline: Lexing → Parsing → Type Checking → Optimization → Code Generation

Error Handling: Comprehensive error reporting with optional debug information

Multiple Output Formats: Support for different output directories and file formats

Integration Ready: Designed for use with build systems and IDEs

Usage

cure input.cure                    # Compile with defaults
cure input.cure -o output.beam     # Specify output file
cure input.cure --verbose          # Enable verbose output
cure input.cure --no-optimize      # Disable optimizations

Command Line Options

-o, --output FILE - Output .beam file path

-d, --output-dir DIR - Output directory (default: _build/ebin)

--verbose - Enable verbose compilation output

--no-debug - Disable debug information in output

--no-warnings - Suppress compiler warnings

--no-type-check - Skip type checking phase

--no-optimize - Disable type-directed optimizations

--help, -h - Show help information

--version, -v - Show version information

Environment Variables

CURE_DEBUG=1 - Enable detailed debug output including stack traces

Error Codes

0 - Success

1 - Compilation or runtime error

2 - Usage error (invalid arguments)

Summary

Functions

add_automatic_stdlib_imports(Source, Options)

check_cure_installation()

Verify that all required Cure compiler modules are available.

compile_file(Filename)

Compile a .cure file with default compilation options.

compile_file(Filename, Options)

Compile a .cure file with specified compilation options.

compile_file_from_shell/1

compile_opts_to_codegen_opts(Options)

Convert CLI compilation options to code generation options.

convert_beam_to_source_path(BeamFile)

ensure_stdlib_available(Options)

Ensure that the Cure standard library is available and compiled.

format_compilation_error/1

format_error/1

get_module_info/1

Extract module information from an Abstract Syntax Tree.

has_explicit_module_or_imports(Source)

help()

Display comprehensive help information for the Cure compiler.

main(Args)

Main entry point for the Cure compiler when used as an escript.

version()

Display version and system information for the Cure compiler.

Functions

add_automatic_stdlib_imports(Source, Options)

check_cure_installation()

Verify that all required Cure compiler modules are available.

This function checks for the presence of core compiler modules to ensure the Cure installation is complete and functional.

Required Modules

cure_lexer - Tokenization engine

cure_parser - AST generation

cure_typechecker - Type checking system

cure_codegen - Code generation

Returns

ok - All required modules are present

{error, {missing_modules, List}} - Some modules are missing

Side Effects

Prints warning messages if modules are missing, including instructions to run make all to build the complete compiler.

Usage

This function is called internally to validate the compiler state before attempting compilation operations.

compile_file(Filename)

Compile a .cure file with default compilation options.

Arguments

Filename - Path to the .cure source file to compile

Returns

{ok, OutputFile} - Successful compilation with output file path

{error, Reason} - Compilation failed with error details

Examples

compile_file("examples/hello.cure").
% => {ok, "_build/ebin/hello.beam"}

compile_file(Filename, Options)

Compile a .cure file with specified compilation options.

This is the main compilation entry point that supports all compiler features including type checking, optimizations, and custom output options.

Arguments

Filename - Path to the .cure source file to compile

Options - Compilation options record with fields:

output_file - Custom output file path (optional)

output_dir - Output directory (default: "_build/ebin")

debug_info - Include debug information (default: true)

warnings - Show warnings (default: true)

verbose - Verbose output (default: false)

type_check - Enable type checking (default: true)

optimize - Enable optimizations (default: true)

fsm_runtime - Include FSM runtime (default: true)

Returns

{ok, OutputFile} - Successful compilation

{error, Reason} - Compilation error with detailed reason

Compilation Pipeline

The function executes a complete 5-stage pipeline:

Lexical Analysis - Tokenize source code

Parsing - Build Abstract Syntax Tree

Type Checking - Verify types and constraints (optional)

Optimization - Type-directed optimizations (optional)

Code Generation - Generate BEAM bytecode

Examples

% Compile with verbose output
Options = #compile_options{verbose = true},
compile_file("src/math.cure", Options).

% Compile without optimizations
Options = #compile_options{optimize = false},
compile_file("debug.cure", Options).

% Custom output file
Options = #compile_options{output_file = "custom.beam"},
compile_file("input.cure", Options).

compile_file_from_shell/1

compile_opts_to_codegen_opts(Options)

Convert CLI compilation options to code generation options.

This function transforms the user-facing compilation options into the internal format expected by the code generation modules.

Arguments

Options - Compilation options record

Returns

List of {Key, Value} tuples for the code generator

Option Mapping

debug_info → {debug_info, true}

optimize → {optimize, 1}

warnings → {warnings, true}

fsm_runtime → {fsm_integration, true}

convert_beam_to_source_path(BeamFile)

ensure_stdlib_available(Options)

Ensure that the Cure standard library is available and compiled.

This function checks if the standard library BEAM files exist, and if not, attempts to compile them automatically.

Arguments

Options - Compilation options including verbosity settings

Returns

ok - Standard library is available

{error, Reason} - Standard library compilation failed

Side Effects

May invoke make stdlib to compile missing standard library

Prints progress messages if verbose mode is enabled

format_compilation_error/1

format_error/1

get_module_info/1

Extract module information from an Abstract Syntax Tree.

Extracts comprehensive metadata from compiled modules including:

Module name

Exported functions with arities

Imported modules

Type definitions

FSM definitions

Function count

Arguments

AST - Abstract Syntax Tree from the parser (list of items or single module_def)

Returns

Map with module information:

name - Module name (atom or 'unknown')

exports - List of exported function specs with name/arity

imports - List of imported module names

functions - List of function names defined in module

types - List of type definition names

fsms - List of FSM definition names

function_count - Total number of functions

type_count - Total number of types

fsm_count - Total number of FSMs

type - Module type ('module' or 'unknown')

Example

AST = cure_parser:parse_file("MyModule.cure"),
Info = get_module_info(AST),
% => #{name => 'MyModule', exports => [{hello, 1}], ...}

has_explicit_module_or_imports(Source)

help()

Display comprehensive help information for the Cure compiler.

Outputs usage instructions, command-line options, examples, and environment variables to assist users in using the compiler effectively.

Output Format

Usage: Basic command syntax

Arguments: Required input file specification

Options: All available command-line flags with descriptions

Examples: Common usage patterns

Environment: Relevant environment variables

main(Args)

Main entry point for the Cure compiler when used as an escript.

This function processes command line arguments and orchestrates the entire compilation process. It handles all user-facing errors and exits with appropriate status codes.

Arguments

Args - List of command line arguments as strings

Exit Codes

0 - Successful compilation

1 - Compilation error or internal error

2 - Usage error (invalid arguments)

Examples

% These calls happen automatically when using the CLI:
main(["input.cure"]).
main(["input.cure", "-o", "output.beam"]).
main(["--help"]).

Error Handling

All exceptions are caught and converted to user-friendly error messages. When CURE_DEBUG=1 is set, full stack traces are displayed for debugging.

version()

Display version and system information for the Cure compiler.

Shows the current Cure compiler version, Erlang/OTP version, and a brief description of the Cure programming language.

Output Information

Cure Version: Current compiler version (from ?CURE_VERSION)

Erlang/OTP Version: Version of the runtime platform

Description: Brief overview of Cure language features

Example Output

Cure Programming Language Compiler v0.1.0

Built with Erlang/OTP 25

Cure is a dependently-typed functional programming language
for the BEAM virtual machine with built-in finite state machines.

cure_codegen

Cure Programming Language - BEAM Code Generator

The code generator transforms typed Cure AST into BEAM bytecode, enabling Cure programs to run on the Erlang Virtual Machine. It handles all Cure language features including dependent types, finite state machines, pattern matching, and integration with Erlang/OTP.

Features

Complete Language Support

Module Compilation: Full module support with imports/exports

Function Compilation: Regular and dependent function types

Expression Compilation: All Cure expressions to BEAM instructions

Pattern Matching: Efficient pattern compilation with optimization

Type Integration: Uses type information for optimizations

FSM Code Generation

Native FSM Support: Compiles FSMs to gen_statem behaviors

State Optimization: Optimizes state transitions and data access

Guard Compilation: Efficient guard expression compilation

Action Compilation: Action sequences to BEAM instructions

BEAM Integration

Bytecode Generation: Direct BEAM bytecode emission

Module Attributes: Proper module metadata generation

Export Lists: Correct function export handling

Debug Information: Optional debug info generation

Optimization Features

Configurable Levels: Multiple optimization levels (0-3)

Type-directed: Uses type information for better code

Dead Code Elimination: Removes unused code paths

Instruction Optimization: BEAM instruction-level optimizations

Compilation Pipeline

1. Program Compilation

%% Compile entire program
{ok, Modules} = cure_codegen:compile_program(AST),

%% With custom options
Options = [{optimize, 2}, {debug_info, true}],
{ok, Modules} = cure_codegen:compile_program(AST, Options).

2. Module Compilation

%% Compile single module
Module = #module_def{name = 'MyModule', exports = Exports, items = Items},
{ok, CompiledModule} = cure_codegen:compile_module(Module),

%% Generate BEAM file
cure_codegen:write_beam_module(CompiledModule, "MyModule.beam").

3. Function Compilation

%% Compile individual function
Func = #function_def{name = add, params = Params, body = Body},
{ok, CompiledFunc, State} = cure_codegen:compile_function(Func).

Code Generation Process

Phase 1: AST Analysis

Type Information: Extract and validate type annotations

Import Resolution: Process module imports and dependencies

Export Analysis: Validate and process export specifications

Dependency Analysis: Build function dependency graph

Phase 2: Instruction Generation

Expression Compilation: Convert expressions to BEAM instructions

Pattern Compilation: Generate efficient pattern matching code

Guard Compilation: Compile guard expressions

Control Flow: Generate conditionals, loops, and jumps

Phase 3: Optimization

Instruction Optimization: Peephole optimizations

Register Allocation: Efficient register usage

Jump Optimization: Minimize jumps and labels

Constant Folding: Compile-time constant evaluation

Phase 4: Module Assembly

Function Assembly: Combine compiled functions

Attribute Generation: Create module attributes

Export List: Generate proper export specifications

BEAM File: Produce final BEAM bytecode file

Compilation Options

Standard Options

Options = [
    {debug_info, true},      % Include debug information
    {optimize, 2},           % Optimization level 0-3
    {warnings, true},        % Enable compilation warnings
    {strict_types, true},    % Strict type checking
    {fsm_integration, true}  % Enable FSM features
].

Optimization Levels

Level 0: No optimizations (fastest compile, debugging)

Level 1: Basic optimizations (safe, minimal impact)

Level 2: Standard optimizations (default, balanced)

Level 3: Aggressive optimizations (maximum performance)

Expression Compilation

Literals

42          → {integer, 42}
"hello"     → {string, "hello"}
true        → {atom, true}
[1,2,3]     → {cons, {integer,1}, {cons, {integer,2}, ...}}

Function Calls

foo(x, y)   → {call, {atom, foo}, [VarX, VarY]}
Mod.func(x) → {call, {remote, {atom, 'Mod'}, {atom, func}}, [VarX]}

Pattern Matching

match value do
    {ok, x} -> x
    error -> 0
end

Compiles to efficient jump table with pattern tests.

FSM Compilation

Finite state machines compile to standard Erlang gen_statem:

fsm Counter do
    states: [idle, counting]
    initial: idle

    state idle do
        event start -> counting
    end
end

Generates:

init/1 callback for initialization

State callback functions for each state

Event handling with pattern matching

State data management

Error Handling

The code generator provides detailed error information:

Compilation Errors: Unsupported constructs, type mismatches

Generation Errors: BEAM instruction generation failures

Optimization Errors: Failed optimizations (non-fatal)

File I/O Errors: BEAM file writing errors

Integration with Type System

Uses type information for:

Type Erasure: Remove type annotations while preserving semantics

Optimization: Type-directed optimizations and specializations

Error Prevention: Catch type-related errors during compilation

Runtime Checks: Generate minimal runtime type checks where needed

BEAM Compatibility

Generates standard BEAM bytecode compatible with:

Erlang/OTP: Full compatibility with Erlang runtime

Elixir: Can be called from Elixir code

LFE/Gleam: Compatible with other BEAM languages

Standard Tools: Works with standard BEAM tools (debugger, profiler)

Performance Characteristics

Compilation Speed: Linear in program size for most constructs

Generated Code: Comparable performance to hand-written Erlang

Memory Usage: Efficient memory usage during compilation

Optimization Impact: 10-40% performance improvement at higher levels

Thread Safety

The code generator is stateless at the module level and can safely compile multiple modules concurrently. Individual function compilation maintains local state that is not shared between threads.

Summary

Functions

compile_expression(Expr)

Compiles a Cure expression to BEAM instructions using default state.

compile_expression(Expr, State)

compile_fsm_impl/2

Compiles a finite state machine definition to BEAM runtime functions.

compile_function(FunctionAST)

Compiles a single Cure function to BEAM bytecode using default options.

compile_function/2

compile_module(ModuleAST)

Compiles a single Cure module to BEAM bytecode using default options.

compile_module/2

compile_patterns_to_case_clauses(Patterns, State)

compile_program(AST)

Compiles a complete Cure program to BEAM bytecode using default options.

compile_program(AST, Options)

compile_value_to_erlang_form(Value, Location)

convert_body_expression_to_erlang/2

convert_list_pattern_to_erlang_form/3

convert_pattern_to_erlang_form/2

convert_to_erlang_forms(Module)

default_options()

generate_beam_file(Module, OutputPath)

Generates a BEAM bytecode file from a compiled Cure module.

generate_fsm_functions(FSMName, CompiledFSM, Location)

generate_module_attributes(State)

new_state()

validate_options(Options)

write_beam_module(Module, OutputPath)

Writes a compiled Cure module to a BEAM file.

Functions

compile_expression(Expr)

Compiles a Cure expression to BEAM instructions using default state.

This is the main expression compilation entry point that handles conversion of all Cure expression types to equivalent BEAM bytecode instructions.

Arguments

Expr - Expression AST node (various expr record types)

Returns

{Instructions, State} - BEAM instructions and updated compilation state

{error, Reason} - Compilation error details

Example

Expr = #binary_op_expr{op = '+', left = {literal, 5}, right = {literal, 3}},
{Instructions, _State} = cure_codegen:compile_expression(Expr).

Supported Expression Types

Literals (integers, atoms, strings, booleans)

Identifiers (variables, function references)

Binary operations (arithmetic, logical, comparison)

Function calls (local and remote)

Control flow (if/else, pattern matching)

Data structures (lists, tuples, records)

Lambda expressions and blocks

String interpolation

Type annotations

Error Handling

Returns detailed error information for unsupported expressions, type mismatches, and compilation failures.

compile_expression(Expr, State)

compile_fsm_impl/2

Compiles a finite state machine definition to BEAM runtime functions.

This function transforms a Cure FSM definition into executable BEAM code that integrates with the FSM runtime system. It generates helper functions for spawning, controlling, and querying FSM instances.

Arguments

FSMDef - FSM definition AST node (#fsm_def{})

State - Current compilation state

Returns

{ok, {fsm, CompiledFSM}, NewState} - Successfully compiled FSM

{error, Reason} - Compilation error details

Generated Functions

For an FSM named Counter, generates:

Counter_spawn/0 - Spawn FSM with default initial state

Counter_spawn/1 - Spawn FSM with custom initial data

Counter_send/2 - Send event to FSM instance

Counter_state/1 - Get current state of FSM instance

Counter_stop/1 - Stop FSM instance gracefully

Counter_definition/0 - Get compiled FSM definition

Example

FSM = #fsm_def{
    name = 'Counter',
    states = [idle, counting],
    initial = idle,
    state_defs = [IdleState, CountingState]
},
{ok, {fsm, CompiledFSM}, NewState} = compile_fsm_impl(FSM, State).

FSM Runtime Integration

Compiles FSM to cure_fsm_runtime format

Generates proper BEAM bytecode for FSM operations

Integrates with gen_statem behavior patterns

Handles state transitions, events, and timeouts

Provides type-safe FSM interface functions

State Management

FSMs maintain state data through:

Initial state setup from spawn parameters

State data transformation during transitions

Event payload integration with state data

Timeout handling with state persistence

compile_function(FunctionAST)

Compiles a single Cure function to BEAM bytecode using default options.

This function handles standalone function compilation, primarily used for testing and development. In normal compilation, functions are compiled as part of module compilation.

Arguments

FunctionAST - Function AST node (function_def record or tuple format)

Returns

{ok, CompiledFunction, State} - Successfully compiled function with state

{error, Reason} - Compilation error details

Example

FuncAST = #function_def{
    name = add,
    params = [x, y],
    body = {binary_op, '+', {var, x}, {var, y}}
},
{ok, CompiledFunc, _State} = cure_codegen:compile_function(FuncAST).

Function Processing

Converts function parameters to BEAM registers

Compiles function body expressions to BEAM instructions

Handles pattern matching in parameters

Generates proper function entry and exit code

Applies function-level optimizations

Limitations

Creates minimal compilation state for standalone compilation

May not have access to full module context for imports/types

Primarily intended for testing individual functions

compile_function/2

compile_module(ModuleAST)

Compiles a single Cure module to BEAM bytecode using default options.

This function handles compilation of complete module definitions including exports, imports, function definitions, FSM definitions, and type definitions. It converts Cure module AST to BEAM-compatible Erlang forms.

Arguments

ModuleAST - Module AST node (module_def record or tuple format)

Returns

{ok, CompiledModule} - Successfully compiled module ready for BEAM

{error, Reason} - Compilation error with details

Example

ModuleAST = #module_def{
    name = 'MyModule',
    exports = [{foo, 2}, {bar, 1}],
    items = [FuncDef1, FuncDef2]
},
{ok, BeamModule} = cure_codegen:compile_module(ModuleAST),
cure_codegen:write_beam_module(BeamModule, "MyModule.beam").

Module Processing

Processes imports and builds import environment

Validates and converts export specifications

Compiles all module items (functions, FSMs, types)

Generates proper BEAM module structure with attributes

Handles both old and new AST formats for compatibility

Supported Module Items

Function definitions (regular and Erlang functions)

FSM definitions (compiled to gen_statem)

Record and type definitions

Import and export declarations

compile_module/2

compile_patterns_to_case_clauses(Patterns, State)

compile_program(AST)

Compiles a complete Cure program to BEAM bytecode using default options.

This is a convenience function that calls compile_program/2 with default compilation options.

Arguments

AST - List of top-level AST items (modules, functions, etc.)

Returns

{ok, Modules} - Successfully compiled modules

{error, {compilation_failed, Errors}} - Compilation failures

Example

AST = cure_parser:parse_file("program.cure"),
{ok, Modules} = cure_codegen:compile_program(AST),
lists:foreach(fun(Module) ->
    cure_codegen:write_beam_module(Module, filename(Module))
end, Modules).

Default Options

Uses standard compilation options: debug_info, optimization level 1, warnings enabled, strict types, and FSM integration.

compile_program(AST, Options)

compile_value_to_erlang_form(Value, Location)

convert_body_expression_to_erlang/2

convert_list_pattern_to_erlang_form/3

convert_pattern_to_erlang_form/2

convert_to_erlang_forms(Module)

default_options()

generate_beam_file(Module, OutputPath)

Generates a BEAM bytecode file from a compiled Cure module.

This function converts the internal compiled module representation to standard Erlang abstract forms, then uses the Erlang compiler to produce a BEAM bytecode file compatible with the Erlang Virtual Machine.

Arguments

Module - Compiled module data (map with functions, exports, etc.)

OutputPath - File path where BEAM file should be written

Returns

{ok, {ModuleName, OutputPath}} - Successfully generated BEAM file

{error, Reason} - Generation error details

Example

{ok, CompiledModule} = cure_codegen:compile_module(ModuleAST),
{ok, {MyModule, "MyModule.beam"}} =
    cure_codegen:generate_beam_file(CompiledModule, "MyModule.beam").

Process Steps

Form Conversion: Convert internal representation to Erlang forms

Erlang Compilation: Use Erlang compiler to generate bytecode

File Writing: Write binary BEAM data to specified path

Error Handling: Provide detailed errors at each step

BEAM Compatibility

Generated BEAM files are fully compatible with:

Standard Erlang/OTP runtime

Elixir and other BEAM languages

BEAM development and debugging tools

Hot code reloading and distribution

Error Types

{write_failed, Reason} - File system errors

{compile_failed, Errors, Warnings} - Erlang compiler errors

Form conversion errors from convert_to_erlang_forms/1

generate_fsm_functions(FSMName, CompiledFSM, Location)

generate_module_attributes(State)

new_state()

validate_options(Options)

write_beam_module(Module, OutputPath)

Writes a compiled Cure module to a BEAM file.

This is a convenience function that calls generate_beam_file/2 to convert a compiled module to BEAM bytecode and write it to the specified path.

Arguments

Module - Compiled module data from compile_module/1,2

OutputPath - File path where BEAM file should be written

Returns

{ok, {ModuleName, OutputPath}} - Successfully written BEAM file

{error, Reason} - File writing or compilation error

Example

{ok, CompiledModule} = cure_codegen:compile_module(AST),
{ok, {MyModule, "MyModule.beam"}} =
    cure_codegen:write_beam_module(CompiledModule, "MyModule.beam"),

%% Load and test the module
code:load_file(MyModule),
MyModule:function_name(args).

Use Cases

Final step in Cure compilation pipeline

Integration with build systems and tools

Deployment of Cure modules to BEAM environments

Testing and development workflows

cure_compile_wrapper

Summary

Functions

compile_source_file(SourceFile)

compile_source_file(SourceFile, Options)

format_error(Error)

get_error_suggestions(Error)

Functions

compile_source_file(SourceFile)

compile_source_file(SourceFile, Options)

format_error(Error)

get_error_suggestions(Error)

cure_error_reporter

Cure Error Reporter

Enhanced error reporting module with precise location tracking and user-friendly diagnostic messages. This module provides rich error formatting for parser, lexer, and semantic analysis errors.

Features

Rich Location Info: Line, column, and file context

Snippet Display: Show source code around errors

Suggestions: Provide helpful hints for common mistakes

Color Formatting: Terminal color support for better readability

Multi-error Support: Report multiple errors in batch

Summary

Functions

create_diagnostic(Severity, Location, Message, Suggestions)

format_error(Error, Location)

format_error/3

format_parse_error(Reason, Line, Column, File)

format_type_error(Reason, Location, Expected, Got)

format_with_snippet/3

Functions

create_diagnostic(Severity, Location, Message, Suggestions)

-spec create_diagnostic(error | warning | info,
                        #location{line :: term(), column :: term(), file :: term()},
                        binary(),
                        [binary()]) ->
                           #diagnostic{severity :: error | warning | info,
                                       location ::
                                           #location{line :: term(), column :: term(), file :: term()},
                                       message :: binary(),
                                       snippet :: binary() | undefined,
                                       suggestions :: [binary()]}.

format_error(Error, Location)

-spec format_error(term(), #location{line :: term(), column :: term(), file :: term()}) -> binary().

format_error/3

-spec format_error(term(), #location{line :: term(), column :: term(), file :: term()}, map()) ->
                      binary().

format_parse_error(Reason, Line, Column, File)

-spec format_parse_error(term(), integer(), integer(), string() | undefined) -> binary().

format_type_error(Reason, Location, Expected, Got)

-spec format_type_error(term(),
                        #location{line :: term(), column :: term(), file :: term()},
                        term(),
                        term()) ->
                           binary().

format_with_snippet/3

-spec format_with_snippet(term(), #location{line :: term(), column :: term(), file :: term()}, binary()) ->
                             binary().

cure_fsm_builtins

Cure Programming Language - FSM Built-in Functions

This module provides built-in FSM functions that interface directly with the cure_fsm_runtime module. These functions are called from Cure programs via the FFI (Foreign Function Interface) to provide FSM functionality.

Features

FSM Lifecycle Management

FSM Spawning: Create new FSM instances with type validation

FSM Termination: Graceful shutdown of FSM processes

FSM Operations

Event Sending: Asynchronous event dispatch to FSMs

State Inspection: Query current FSM state and information

Batch Operations: Efficient batch event processing

FSM Utilities

Process Monitoring: Monitor FSM processes for termination

Process Linking: Bidirectional crash propagation

Timeout Management: Set and clear FSM timeouts

API Design

All functions are designed to be called from Cure programs via FFI. They provide a clean interface to the underlying Erlang FSM runtime.

Summary

Functions

fsm_clear_timeout/1

fsm_get_performance_stats/1

fsm_get_registered_types()

fsm_history/1

fsm_info/1

fsm_is_alive/1

fsm_link/1

fsm_lookup_definition/1

fsm_monitor/1

fsm_reset_stats/1

fsm_send/2

fsm_send/3

fsm_send_batch/2

fsm_set_data/2

fsm_set_timeout/3

fsm_spawn/2

fsm_spawn_with_options/3

fsm_state/1

fsm_stop/1

fsm_unlink/1

fsm_validate_event/2

fsm_validate_type/1

register_fsm_builtins(Env)

validate_fsm_event(FSMPid, Event)

validate_fsm_type(FSMType)

Functions

fsm_clear_timeout/1

fsm_get_performance_stats/1

fsm_get_registered_types()

fsm_history/1

fsm_info/1

fsm_is_alive/1

fsm_link/1

fsm_lookup_definition/1

fsm_monitor/1

fsm_reset_stats/1

fsm_send/2

fsm_send/3

fsm_send_batch/2

fsm_set_data/2

fsm_set_timeout/3

fsm_spawn/2

fsm_spawn_with_options/3

fsm_state/1

fsm_stop/1

fsm_unlink/1

fsm_validate_event/2

fsm_validate_type/1

register_fsm_builtins(Env)

validate_fsm_event(FSMPid, Event)

validate_fsm_type(FSMType)

cure_fsm_cure_api

Cure FSM API Wrapper

This module provides the Cure-level FSM API that matches the design in lib/std/fsm.cure. It wraps the underlying cure_fsm_runtime gen_server to provide:

start_fsm/1: Start an FSM instance from a module

fsm_cast/2: Send events asynchronously

fsm_advertise/2: Register a name for an FSM

fsm_state/1: Query current state and payload

The FSM definitions in Cure modules are compiled to:

A record type for the payload

A list of transitions with handler functions

An initial state and initial payload

This module bridges the gap between Cure's high-level FSM syntax and the Erlang gen_server runtime.

Summary

Functions

fsm_advertise(Pid, Name)

fsm_cast(Target, Event)

fsm_state(Target)

start_fsm(Module)

Functions

fsm_advertise(Pid, Name)

-spec fsm_advertise(Pid :: pid(), Name :: atom()) -> ok | {error, term()}.

fsm_cast(Target, Event)

-spec fsm_cast(Target :: pid() | atom(), Event :: {atom(), list()}) -> ok.

fsm_state(Target)

-spec fsm_state(Target :: pid() | atom()) -> {ok, {atom(), term()}} | {error, term()}.

start_fsm(Module)

-spec start_fsm(Module :: atom()) -> {ok, pid()} | {error, term()}.

cure_fsm_runtime

Cure Programming Language - FSM Runtime System

The FSM runtime system provides a comprehensive execution environment for finite state machines in the Cure programming language. It implements a complete FSM execution model with state transitions, guard evaluation, action execution, and performance optimizations, all built on top of the BEAM virtual machine.

Core Features

FSM Process Management

FSM Lifecycle: Complete process management with start/stop operations

Event Processing: Synchronous and asynchronous event handling

Batch Operations: Optimized batch event processing for performance

State Inspection: Runtime state introspection and debugging support

Execution Engine

Guard Compilation: Compiled guard expressions with instruction-based evaluation

Action System: Compiled action execution with state mutation support

Transition Engine: Optimized state transition processing with O(1) lookup

Timeout Support: Built-in timeout handling with automatic state transitions

Performance Optimizations

Compiled Guards/Actions: Pre-compiled instruction sequences for efficiency

Flat Transition Maps: O(1) transition lookup using optimized data structures

Memory Management: Automatic event history trimming to prevent memory leaks

Performance Statistics: Real-time performance monitoring and metrics

Registry System

FSM Type Registration: Global registry for FSM type definitions

Dynamic Lookup: Runtime FSM definition resolution

Type Management: Registration, unregistration, and type enumeration

Architecture

The FSM runtime is built as a gen_server behavior that manages individual FSM instances. Each FSM process maintains its own state, transition table, timeout handlers, and performance statistics.

%% Start a traffic light FSM
{ok, FSM} = cure_fsm_runtime:start_fsm(traffic_light, #{}).

%% Send events to the FSM
cure_fsm_runtime:send_event(FSM, timer_expired),
cure_fsm_runtime:send_event(FSM, emergency_stop).

%% Get current state
{ok, State} = cure_fsm_runtime:get_state(FSM).

Event Processing Model

Events are processed through a multi-stage pipeline:

Event Reception: Events arrive via gen_server casts/calls

Transition Lookup: O(1) lookup in flat transition map

Guard Evaluation: Compiled guard instruction execution

Action Execution: Compiled action instruction execution with state updates

State Transition: Atomic state change with history tracking

Timeout Management: Automatic timeout setting/clearing

Compilation Pipeline

FSM definitions undergo compilation from AST to optimized runtime format:

Transition Compilation: Nested AST transitions → flat lookup maps

Guard Compilation: AST expressions → instruction sequences

Action Compilation: AST actions → stack-based instructions

Timeout Compilation: Timeout definitions → runtime timeout handlers

Performance Characteristics

Event Processing: < 10μs per event (compiled guards/actions)

State Transitions: O(1) lookup time

Memory Usage: Bounded with automatic history trimming

Throughput: > 100K events/second per FSM instance

Batch Processing: Up to 10x improvement for bulk operations

Error Handling

The runtime provides comprehensive error handling:

Guard Failures: Safe evaluation with automatic fallback to false

Action Errors: Safe execution with state preservation on failure

Timeout Handling: Robust timeout management with cleanup

Type Safety: Runtime type checking and validation

Integration

The FSM runtime integrates with:

Cure Compiler: Receives compiled FSM definitions from type checker

Guard Compiler: Uses compiled guard expressions for efficiency

Action Compiler: Executes compiled action instruction sequences

BEAM Runtime: Built on standard OTP gen_server behavior

Summary

Functions

clear_fsm_registry()

Clears all FSM type definitions from the global registry.

clear_timeout(FSMPid)

Clears any existing timeout for the FSM.

code_change(OldVsn, State, Extra)

compile_fsm_definition(FSMDef)

Compiles an FSM definition from AST format to optimized runtime format.

get_current_state(FSMPid)

get_fsm_info(FSMPid)

Retrieves comprehensive FSM information for debugging and introspection.

get_performance_stats(FSMPid)

Retrieves performance statistics for an FSM instance.

get_registered_fsm_types()

Returns a list of all registered FSM type names.

get_state(FSMPid)

Retrieves the current state of an FSM instance.

handle_call/3

handle_cast/2

handle_info/2

init/1

list_running_fsms()

lookup_fsm/1

lookup_fsm_definition(FSMType)

Looks up an FSM definition by type name in the global registry.

receive_message(FsmPid)

receive_message(FsmPid, Timeout)

register_fsm_type(FSMType, Definition)

Registers a new FSM type definition in the global registry.

register_fsm_type(FSMType, States, InitialState, Transitions)

send_batch_events(FSMPid, Events)

Sends multiple events to an FSM in a single operation for improved performance.

send_event(FSMPid, Event)

Sends an event to an FSM instance without event data.

send_event(FSMPid, Event, Data)

Sends an event with associated data to an FSM instance.

send_message(FsmPid, Message)

send_message(FsmPid, Message, Options)

set_timeout(FSMPid, Timeout, Event)

Sets a timeout for the FSM that will trigger the specified event after the given time.

spawn_fsm(FSMType)

spawn_fsm(FsmType, FsmDef, InitArgs)

spawn_fsm(FsmType, FsmDef, InitArgs, Options)

start_fsm(FSMType, InitialData)

Starts a new FSM instance with the specified type and initial data.

start_fsm(FSMType, InitialData, Options)

Starts a new FSM instance with the specified type, initial data, and options.

stop_fsm(FSMPid)

Stops an FSM instance gracefully.

terminate/2

unregister_fsm_type(FSMType)

Removes an FSM type definition from the global registry.

Functions

clear_fsm_registry()

Clears all FSM type definitions from the global registry.

Returns

ok - Registry cleared successfully

Warning

This function removes ALL registered FSM types. Use with caution.

Example

cure_fsm_runtime:clear_fsm_registry().

clear_timeout(FSMPid)

Clears any existing timeout for the FSM.

Arguments

FSMPid - The PID of the FSM process

Returns

ok - Timeout cleared successfully (asynchronous)

Example

cure_fsm_runtime:clear_timeout(FSMPid).

code_change(OldVsn, State, Extra)

compile_fsm_definition(FSMDef)

Compiles an FSM definition from AST format to optimized runtime format.

This function transforms a parsed FSM definition into an efficient runtime representation with pre-compiled guards, actions, and optimized transition lookups.

Arguments

FSMDef - FSM definition record from the parser containing:

name - FSM type name

states - List of state names

initial - Initial state name

state_defs - List of state definition records

Returns

#fsm_definition{} - Compiled FSM definition ready for runtime execution

Compilation Process

Transition Compilation: Creates flat lookup maps from nested AST

Guard Compilation: Compiles guard expressions to instruction sequences

Action Compilation: Compiles action expressions to stack-based instructions

Timeout Compilation: Extracts and organizes timeout definitions

Example

CompiledDef = cure_fsm_runtime:compile_fsm_definition(ParsedFSM),
cure_fsm_runtime:register_fsm_type(my_fsm, CompiledDef).

get_current_state(FSMPid)

get_fsm_info(FSMPid)

Retrieves comprehensive FSM information for debugging and introspection.

Arguments

FSMPid - The PID of the FSM process

Returns

{ok, Info} - Map containing FSM information:

fsm_type - The FSM type name

current_state - Current state name

data - Current state data

event_history - List of recent events (newest first)

{error, Reason} - Error retrieving information

Example

{ok, #{fsm_type := Type, current_state := State}} =
    cure_fsm_runtime:get_fsm_info(FSMPid).

get_performance_stats(FSMPid)

Retrieves performance statistics for an FSM instance.

Arguments

FSMPid - The PID of the FSM process

Returns

{ok, Stats} - Performance statistics record containing:

events_processed - Total number of events processed

avg_event_time - Average event processing time (microseconds)

max_event_time - Maximum event processing time (microseconds)

memory_usage - Current memory usage (bytes)

last_updated - Timestamp of last update

{error, Reason} - Error retrieving statistics

Example

{ok, Stats} = cure_fsm_runtime:get_performance_stats(FSMPid),
AvgTime = Stats#fsm_perf_stats.avg_event_time.

get_registered_fsm_types()

Returns a list of all registered FSM type names.

Returns

List of FSM type names (atoms)

Example

Types = cure_fsm_runtime:get_registered_fsm_types(),
%% Types might be [counter, traffic_light, state_machine]

get_state(FSMPid)

Retrieves the current state of an FSM instance.

Arguments

FSMPid - The PID of the FSM process

Returns

{ok, State} - The current state name (atom)

{error, Reason} - Error retrieving state

Example

{ok, CurrentState} = cure_fsm_runtime:get_state(FSMPid).

handle_call/3

handle_cast/2

handle_info/2

init/1

list_running_fsms()

lookup_fsm/1

lookup_fsm_definition(FSMType)

Looks up an FSM definition by type name in the global registry.

Arguments

FSMType - The FSM type name to look up (atom)

Returns

{ok, Definition} - FSM definition found

{error, not_found} - FSM type not registered

Example

case cure_fsm_runtime:lookup_fsm_definition(counter) of
    {ok, Definition} -> cure_utils:debug("Found FSM definition~n");
    {error, not_found} -> cure_utils:debug("FSM type not registered~n")
end.

receive_message(FsmPid)

receive_message(FsmPid, Timeout)

register_fsm_type(FSMType, Definition)

Registers a new FSM type definition in the global registry.

Arguments

FSMType - The FSM type name (atom)

Definition - Compiled FSM definition record

Returns

ok - FSM type registered successfully

Example

Definition = #fsm_definition{name = counter, ...},
ok = cure_fsm_runtime:register_fsm_type(counter, Definition).

register_fsm_type(FSMType, States, InitialState, Transitions)

send_batch_events(FSMPid, Events)

Sends multiple events to an FSM in a single operation for improved performance.

Arguments

FSMPid - The PID of the FSM process

Events - List of events to send. Each event can be:

An atom (event without data)

A tuple {Event, Data} (event with data)

Returns

ok - Batch sent successfully (asynchronous)

Performance

Batch processing can provide 5-10x performance improvement over individual event sends when processing large numbers of events.

Example

Events = [start, {increment, 5}, stop],
cure_fsm_runtime:send_batch_events(FSMPid, Events).

send_event(FSMPid, Event)

Sends an event to an FSM instance without event data.

This is a convenience function that calls send_event/3 with undefined event data.

Arguments

FSMPid - The PID of the target FSM process

Event - The event to send (atom)

Returns

ok - Event sent successfully (asynchronous)

Example

cure_fsm_runtime:send_event(FSMPid, start).

send_event(FSMPid, Event, Data)

Sends an event with associated data to an FSM instance.

Arguments

FSMPid - The PID of the target FSM process

Event - The event to send (atom)

Data - Event data to accompany the event

Returns

ok - Event sent successfully (asynchronous)

Example

cure_fsm_runtime:send_event(FSMPid, button_pressed, #{button => ok}).

send_message(FsmPid, Message)

send_message(FsmPid, Message, Options)

set_timeout(FSMPid, Timeout, Event)

Sets a timeout for the FSM that will trigger the specified event after the given time.

Arguments

FSMPid - The PID of the FSM process

Timeout - Timeout in milliseconds

Event - Event to trigger when timeout occurs

Returns

ok - Timeout set successfully (asynchronous)

Example

cure_fsm_runtime:set_timeout(FSMPid, 5000, timeout_expired).

spawn_fsm(FSMType)

spawn_fsm(FsmType, FsmDef, InitArgs)

spawn_fsm(FsmType, FsmDef, InitArgs, Options)

start_fsm(FSMType, InitialData)

Starts a new FSM instance with the specified type and initial data.

This is a convenience function that calls start_fsm/3 with an empty options list.

Arguments

FSMType - The registered FSM type name (atom)

InitialData - Initial state data for the FSM instance

Returns

{ok, Pid} - Success with the FSM process PID

{error, {fsm_type_not_found, FSMType}} - FSM type not registered

{error, Reason} - Other gen_server startup errors

Example

{ok, FSM} = cure_fsm_runtime:start_fsm(counter, #{count => 0}).

start_fsm(FSMType, InitialData, Options)

Starts a new FSM instance with the specified type, initial data, and options.

Arguments

FSMType - The registered FSM type name (atom)

InitialData - Initial state data for the FSM instance

Options - List of startup options (currently unused)

Returns

{ok, Pid} - Success with the FSM process PID

{error, {fsm_type_not_found, FSMType}} - FSM type not registered

{error, Reason} - Other gen_server startup errors

Example

{ok, FSM} = cure_fsm_runtime:start_fsm(traffic_light, #{}, []).

stop_fsm(FSMPid)

Stops an FSM instance gracefully.

Arguments

FSMPid - The PID of the FSM process to stop

Returns

ok - FSM stopped successfully

{error, Reason} - Error stopping the FSM

Example

ok = cure_fsm_runtime:stop_fsm(FSMPid).

terminate/2

unregister_fsm_type(FSMType)

Removes an FSM type definition from the global registry.

Arguments

FSMType - The FSM type name to unregister (atom)

Returns

true - FSM type unregistered successfully (or did not exist)

Example

cure_fsm_runtime:unregister_fsm_type(old_counter).

cure_guard_codegen

Guard Validation Code Generation

This module generates runtime validation code for dependent type guards. It translates guard constraints into executable BEAM code that validates values against dependent type requirements.

Features

Dependent Type Validation: Generate checks for dependent type constraints

Optimized Code: Efficient guard code with minimal runtime overhead

SMT Integration: Use SMT solver results to optimize guard checks

Error Reporting: Generate informative error messages for failed guards

Guard Types

Numeric Constraints

Vector(T, n: Nat) when n > 0

Generates: Runtime check that n > 0

Refinement Types

NonEmpty(T) = List(T, n) when n > 0

Generates: Length check for lists

Complex Constraints

Matrix(T, rows: Nat, cols: Nat) when rows > 0 and cols > 0

Generates: Multiple validation checks

Code Generation Strategy

Static Analysis: Use SMT solver to prove constraints at compile time

Runtime Guards: Generate checks for constraints that can't be proven

Optimization: Eliminate redundant checks through dataflow analysis

Caching: Cache validation results for expensive computations

Summary

Types

expr()

Functions

clear_proof_cache()

compile_constraint(Constraint, Env)

generate_guard(Constraint, Env)

generate_guard(Constraint, Env, Opts)

generate_validation_function(TypeName, Params, Constraint)

optimize_guard(GuardAST, Env)

Types

expr()

-type expr() ::
          #literal_expr{value :: term(), location :: term()} |
          #identifier_expr{name :: term(), location :: term()} |
          #function_call_expr{function :: term(), args :: term(), location :: term()} |
          #match_expr{expr :: term(), patterns :: term(), location :: term()} |
          #let_expr{bindings :: term(), body :: term(), location :: term()} |
          #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} |
          #unary_op_expr{op :: term(), operand :: term(), location :: term()} |
          #list_expr{elements :: term(), location :: term()} |
          #tuple_expr{elements :: term(), location :: term()} |
          #record_expr{name :: term(), fields :: term(), location :: term()} |
          #field_access_expr{record :: term(), field :: term(), location :: term()} |
          #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} |
          #lambda_expr{params :: term(), body :: term(), location :: term()} |
          #fsm_spawn_expr{fsm_name :: term(),
                          init_args :: term(),
                          init_state :: term(),
                          location :: term()} |
          #fsm_send_expr{target :: term(), message :: term(), location :: term()} |
          #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} |
          #fsm_state_expr{location :: term()} |
          #qualified_call_expr{trait_name :: term(),
                               type_args :: term(),
                               method_name :: term(),
                               receiver :: term(),
                               args :: term(),
                               location :: term()}.

Functions

clear_proof_cache()

compile_constraint(Constraint, Env)

-spec compile_constraint(expr(), map()) -> {ok, erl_syntax:syntaxTree()} | {error, term()}.

generate_guard(Constraint, Env)

-spec generate_guard(expr(), map()) -> {ok, erl_syntax:syntaxTree()} | {error, term()}.

generate_guard(Constraint, Env, Opts)

-spec generate_guard(expr(), map(), map()) -> {ok, erl_syntax:syntaxTree()} | {error, term()}.

generate_validation_function(TypeName, Params, Constraint)

-spec generate_validation_function(atom(),
                                   [#param{name :: term(), type :: term(), location :: term()}],
                                   expr()) ->
                                      {ok, erl_syntax:syntaxTree()}.

optimize_guard(GuardAST, Env)

-spec optimize_guard(erl_syntax:syntaxTree(), map()) -> erl_syntax:syntaxTree().

cure_guard_compiler

Summary

Functions

compile_guard(Guard, State)

compile_guards(Guards, State)

is_guard_safe(Literal_expr)

optimize_guard(Guard)

Functions

compile_guard(Guard, State)

compile_guards(Guards, State)

is_guard_safe(Literal_expr)

optimize_guard(Guard)

cure_lexer

Cure Programming Language - Lexer

The lexer module provides tokenization services for Cure source code, converting raw text into a structured stream of tokens for the parser. It supports all Cure language constructs including keywords, operators, literals, and comments.

Features

Position Tracking: Every token includes precise line and column information

String Interpolation: Support for #{expr} string interpolation syntax

Multi-character Operators: Recognition of operators like ->, |>, ::, etc.

Comprehensive Literals: Numbers, strings, atoms, and boolean values

Keywords: All Cure language keywords including FSM constructs

Error Recovery: Detailed error reporting with location information

Token Types

The lexer recognizes the following token categories:

Keywords: def, fsm, match, when, etc.

Identifiers: Variable and function names

Literals: Numbers, strings, atoms, booleans

Operators: +, ->, |>, ::, ==, etc.

Delimiters: (), [], {}, ,, ;, etc.

Comments: Line comments starting with #

String Interpolation

Supports string interpolation with #{expression} syntax:

"Hello #{name}!"  % Tokenized as interpolated string

Error Handling

All tokenization errors include precise location information:

{error, {Reason, Line, Column}}

Summary

Functions

scan/1

token_type/1

Extract the type from a token record.

tokenize(Source)

Tokenize a string of Cure source code into a list of tokens.

tokenize_file(Filename)

Tokenize a Cure source file.

Functions

scan/1

-spec scan(string() | binary()) -> {ok, [tuple()]} | {error, term()}.

token_type/1

-spec token_type(#token{type :: atom(), value :: term(), line :: integer(), column :: integer()}) ->
                    atom().

Extract the type from a token record.

This utility function extracts the token type, which is useful for pattern matching and categorizing tokens in the parser.

Arguments

Token - Token record to extract type from

Returns

Atom representing the token type (e.g., def, identifier, number)

Examples

Token = #token{type = identifier, value = <<"add">>, line = 1, column = 5},
token_type(Token).
% => identifier

KeywordToken = #token{type = def, value = def, line = 1, column = 1},
token_type(KeywordToken).
% => def

tokenize(Source)

-spec tokenize(binary()) ->
                  {ok,
                   [#token{type :: atom(), value :: term(), line :: integer(), column :: integer()}]} |
                  {error, term()}.

Tokenize a string of Cure source code into a list of tokens.

This is the main entry point for lexical analysis. It processes the entire input and returns a list of tokens with position information.

Arguments

Source - Binary containing Cure source code to tokenize

Returns

{ok, Tokens} - Successful tokenization with list of token records

{error, {Reason, Line, Column}} - Tokenization error with location

{error, {Error, Reason, Stack}} - Internal error with stack trace

Token Record

Each token is a record with fields:

type - Token type atom (e.g., identifier, number, def)

value - Token value (e.g., variable name, number value)

line - Line number (1-based)

column - Column number (1-based)

Examples

tokenize(<<"def add(x, y) = x + y">>).
% => {ok, [
%      #token{type=def, value=def, line=1, column=1},
%      #token{type=identifier, value= <<"add">>, line=1, column=5},
%      #token{type='(', value='(', line=1, column=8},
%      ...
%    ]}

tokenize(<<"invalid \xff character">>).
% => {error, {invalid_character, 1, 9}}

Error Types

invalid_character - Unrecognized character in input

unterminated_string - String literal without closing quote

invalid_number_format - Malformed numeric literal

unterminated_comment - Block comment without proper termination

tokenize_file(Filename)

-spec tokenize_file(string()) ->
                       {ok,
                        [#token{type :: atom(), value :: term(), line :: integer(), column :: integer()}]} |
                       {error, term()}.

Tokenize a Cure source file.

This is a convenience function that reads a file from disk and tokenizes its contents. It handles file I/O errors and passes the content to the main tokenization function.

Arguments

Filename - Path to the .cure source file to tokenize

Returns

{ok, Tokens} - Successful tokenization with list of token records

{error, {file_error, Reason}} - File I/O error

{error, {Reason, Line, Column}} - Tokenization error with location

Examples

tokenize_file("examples/hello.cure").
% => {ok, [#token{type=def, ...}, ...]}

tokenize_file("nonexistent.cure").
% => {error, {file_error, enoent}}

cure_lsp_server

Cure Language Server Protocol (LSP) Implementation

This module implements the Language Server Protocol for the Cure programming language, providing IDE features like:

Real-time syntax checking

Type inference hints

Go-to-definition

Hover information

Code completion

Diagnostics reporting

LSP Protocol

The server communicates over JSON-RPC 2.0 using stdio or TCP socket.

Features

Implemented

initialize - Server initialization

textDocument/didOpen - Document opened

textDocument/didChange - Document changed

textDocument/didSave - Document saved

textDocument/didClose - Document closed

textDocument/hover - Hover information

textDocument/diagnostic - Real-time diagnostics

Planned

textDocument/completion - Code completion

textDocument/definition - Go to definition

textDocument/references - Find references

textDocument/rename - Symbol renaming

Summary

Functions

code_change(OldVsn, State, Extra)

get_diagnostics(Uri)

handle_call/3

handle_cast/2

handle_info(Info, State)

handle_message(Message)

init(Opts)

start_link()

start_link(Opts)

stop()

terminate(Reason, State)

update_document(Uri, Content)

Functions

code_change(OldVsn, State, Extra)

get_diagnostics(Uri)

-spec get_diagnostics(binary()) -> [map()].

handle_call/3

handle_cast/2

handle_info(Info, State)

handle_message(Message)

-spec handle_message(map()) -> {ok, map()} | {error, term()}.

init(Opts)

start_link()

-spec start_link() -> {ok, pid()} | {error, term()}.

start_link(Opts)

-spec start_link(map()) -> {ok, pid()} | {error, term()}.

stop()

-spec stop() -> ok.

terminate(Reason, State)

update_document(Uri, Content)

-spec update_document(binary(), binary()) -> ok.

cure_parser

Cure Programming Language - Parser

The parser module implements a recursive descent parser that converts tokens from the lexer into an Abstract Syntax Tree (AST). It handles the complete Cure language grammar including modules, functions, finite state machines, types, records, and expressions.

Features

Language Constructs

Modules: Module definitions with exports and imports

Functions: Function definitions with parameters, return types, and guards

FSMs: Finite state machine definitions with states and transitions

Types: User-defined types, records, and type aliases

Expressions: Complete expression parsing including pattern matching

Literals: Numbers, strings, atoms, lists, tuples, and maps

Parser Architecture

Recursive Descent: Top-down parsing with predictive lookahead

Error Recovery: Comprehensive error reporting with location information

Token Stream: Sequential token processing with position tracking

AST Generation: Direct AST construction during parsing

Error Handling

Syntax Errors: Detailed error messages with expected vs. actual tokens

Location Tracking: Line and column information for all parse errors

Error Recovery: Attempts to continue parsing after errors where possible

Structured Errors: Well-formed error tuples for programmatic handling

Grammar Support

The parser supports the complete Cure language grammar:

Top-Level Constructs

module MyModule do
  export [function/2, MyType]

  def function(param1: Type1, param2: Type2) -> ReturnType do
    # Function body
  end

  fsm StateMachine do
    state idle do
      on start -> running
    end
  end
end

Expression Parsing

Arithmetic: +, -, *, /, div, rem

Logical: and, or, not, andalso, orelse

Comparison: ==, /=, <, >, =<, >=

Pattern Matching: Complete pattern support with guards

Function Calls: Local and remote function calls

Data Structures: Lists, tuples, maps, records

Type System Integration

Type Annotations: Function parameters and return types

Type Definitions: User-defined types and aliases

Generic Types: Parameterized types with constraints

Dependent Types: Types that depend on values

API Usage

%% Parse tokens directly
{ok, AST} = cure_parser:parse(Tokens).

%% Parse from file
{ok, AST} = cure_parser:parse_file("example.cure").

%% Handle parse errors
case cure_parser:parse_file("example.cure") of
    {ok, AST} ->
        cure_utils:debug("Parsed successfully~n");
    {error, {parse_error, Reason, Line, Column}} ->
        cure_utils:debug("Parse error at ~p:~p: ~p~n", [Line, Column, Reason])
end.

Parser State

The parser maintains state including:

Token Stream: Current and remaining tokens

Position: Current parsing position for error reporting

Filename: Source file name for error messages

Context: Current parsing context for better error messages

Error Types

The parser can return these error types:

{parse_error, Reason, Line, Column} - Syntax error with location

{expected, TokenType, got, ActualType} - Expected token mismatch

{unexpected_token, TokenType} - Unexpected token in context

{Error, Reason, Stack} - Internal parser errors

Performance Characteristics

Linear Time: O(n) parsing time for well-formed input

Memory Efficient: Streaming token processing

Early Termination: Stops on first syntax error

Lookahead: Minimal lookahead for efficient parsing

Integration

The parser integrates with:

Lexer: Consumes tokens from cure_lexer

AST: Produces AST records defined in cure_ast.hrl

Type Checker: Provides AST input for type checking

Compiler: Part of the complete compilation pipeline

Summary

Functions

parse(Tokens)

Parses a list of tokens into an Abstract Syntax Tree (AST).

parse_file(Filename)

Parses a Cure source file into an Abstract Syntax Tree (AST).

Functions

parse(Tokens)

-spec parse([term()]) -> {ok, cure_ast:program()} | {error, term()}.

Parses a list of tokens into an Abstract Syntax Tree (AST).

This is the main parsing function that takes a list of tokens from the lexer and produces a complete AST representing the Cure program structure.

Arguments

Tokens - List of token records from cure_lexer

Returns

{ok, Program} - Successfully parsed AST program

{error, {parse_error, Reason, Line, Column}} - Syntax error with location

{error, {Error, Reason, Stack}} - Internal parser error

Example

Tokens = cure_lexer:tokenize("def hello() -> :ok end"),
{ok, AST} = cure_parser:parse(Tokens).

Error Handling

The parser provides detailed error information including:

Specific error reason (expected token, unexpected construct, etc.)

Line and column numbers for error location

Full stack trace for internal errors

parse_file(Filename)

-spec parse_file(string()) -> {ok, cure_ast:program()} | {error, term()}.

Parses a Cure source file into an Abstract Syntax Tree (AST).

This convenience function reads and tokenizes a file, then parses the tokens into an AST. It handles both lexical and syntax errors from the complete lexing and parsing pipeline.

Arguments

Filename - Path to the Cure source file to parse

Returns

{ok, Program} - Successfully parsed AST program

{error, {parse_error, Reason, Line, Column}} - Syntax error with location

{error, LexError} - Lexical error from tokenization

{error, {Error, Reason, Stack}} - Internal parser error

Example

case cure_parser:parse_file("examples/hello.cure") of
    {ok, AST} ->
        cure_utils:debug("Successfully parsed file~n");
    {error, {parse_error, Reason, Line, Col}} ->
        cure_utils:debug("Parse error at ~p:~p: ~p~n", [Line, Col, Reason]);
    {error, Reason} ->
        cure_utils:debug("Error: ~p~n", [Reason])
end.

Error Sources

This function can return errors from:

File I/O: File not found, permission errors

Lexical Analysis: Invalid tokens, malformed strings

Syntax Analysis: Grammar violations, unexpected tokens

cure_profiler

Cure Runtime Profiler

Collects runtime execution statistics to guide compiler optimizations. Provides lightweight instrumentation and aggregation of:

Function call counts and frequencies

Hot path detection through call sequences

Type usage patterns at runtime

Memory allocation patterns

Performance metrics

Usage

% Initialize profiling
cure_profiler:start_profiling(),

% Run your code
my_application:run(),

% Collect profile data
ProfileData = cure_profiler:get_profile_data(),

% Use for optimization
OptimizedAST = cure_type_optimizer:optimize_with_profile(AST, ProfileData),

% Stop profiling
cure_profiler:stop_profiling().

Profile Data Format

Profile data is stored as a map with the following structure:

#{
    function_calls => #{FunctionName => CallCount},
    call_sequences => [{Caller, Callee, Count}],
    type_usage => #{Type => UsageCount},
    memory_allocations => #{Function => AllocationSize},
    hot_functions => [FunctionName],
    hot_paths => [[FunctionName]],
    timestamp => Milliseconds
}

Summary

Functions

analyze_profile()

analyze_profile(Opts)

export_profile(Filename)

get_function_stats()

get_hot_functions()

get_hot_functions(N)

get_hot_paths()

get_profile_data()

get_type_usage()

import_profile(Filename)

record_call_sequence(Caller, Callee)

record_function_call(FunctionName)

record_function_call(FunctionName, Count)

record_memory_allocation(FunctionName, Size)

record_type_usage(FunctionName, Type)

reset_profiling()

start_profiling()

start_profiling(Config)

stop_profiling()

Functions

analyze_profile()

-spec analyze_profile() -> map().

analyze_profile(Opts)

-spec analyze_profile(map()) -> map().

export_profile(Filename)

-spec export_profile(file:filename()) -> ok | {error, term()}.

get_function_stats()

-spec get_function_stats() -> map().

get_hot_functions()

-spec get_hot_functions() -> [atom()].

get_hot_functions(N)

-spec get_hot_functions(pos_integer()) -> [atom()].

get_hot_paths()

-spec get_hot_paths() -> [[atom()]].

get_profile_data()

-spec get_profile_data() -> map().

get_type_usage()

-spec get_type_usage() -> map().

import_profile(Filename)

-spec import_profile(file:filename()) -> ok | {error, term()}.

record_call_sequence(Caller, Callee)

-spec record_call_sequence(atom(), atom()) -> ok.

record_function_call(FunctionName)

-spec record_function_call(atom()) -> ok.

record_function_call(FunctionName, Count)

-spec record_function_call(atom(), pos_integer()) -> ok.

record_memory_allocation(FunctionName, Size)

-spec record_memory_allocation(atom(), non_neg_integer()) -> ok.

record_type_usage(FunctionName, Type)

-spec record_type_usage(atom(), term()) -> ok.

reset_profiling()

-spec reset_profiling() -> ok.

start_profiling()

-spec start_profiling() -> ok.

start_profiling(Config)

-spec start_profiling(map()) -> ok.

stop_profiling()

-spec stop_profiling() -> ok.

cure_runtime

Cure Programming Language - Runtime Execution Engine

The runtime execution engine interprets and executes BEAM instructions generated by the Cure compiler. It provides a complete execution environment for Cure programs with stack-based instruction processing, function calls, module loading, and integration with the Erlang standard library.

Features

Instruction Execution

Stack-based VM: Uses an execution stack for operand management

BEAM Instructions: Processes compiler-generated BEAM instructions

Control Flow: Supports jumps, labels, conditionals, and function calls

Pattern Matching: Handles pattern matching operations

Lambda Functions: Creates and executes anonymous functions

Function System

Module Loading: Loads compiled Cure modules into runtime state

Function Resolution: Resolves and calls both internal and external functions

Parameter Binding: Maps function parameters to argument values

Standard Library: Built-in integration with cure_std functions

Global Functions: Pre-loaded standard functions accessible from any context

Memory Management

Runtime State: Maintains execution state with stack, locals, and parameters

Module Registry: Tracks loaded modules and their functions

Variable Scoping: Separate scopes for parameters, local variables, and globals

Stack Operations: Efficient stack manipulation for all operations

Error Handling

Instruction Errors: Detailed error reporting for instruction execution

Function Errors: Comprehensive function call error handling

Stack Errors: Stack underflow and overflow detection

External Errors: Error propagation from external function calls

Runtime Architecture

Execution Model

The runtime uses a stack-based execution model where:

Instructions operate on an execution stack

Operands are pushed/popped from the stack

Results are left on the stack for subsequent operations

Functions execute with isolated parameter and local variable scopes

State Management

#runtime_state{
    stack = [],      % Execution stack for operands
    locals = #{},    % Local variables in current scope
    params = #{},    % Function parameters
    modules = #{},   % Loaded modules
    globals = #{}    % Global function registry
}

Instruction Set

Supported BEAM instruction types:

Load Operations: load_literal, load_param, load_local, load_global

Store Operations: store_local

Arithmetic: binary_op, unary_op with standard operators

Control Flow: jump, jump_if_false, label, return

Function Calls: call, monadic_pipe_call

Data Structures: make_list, make_lambda

Stack Management: pop, pattern_match

Usage Examples

Basic Program Execution

%% Execute a compiled module
{ok, CompiledModule} = cure_codegen:compile_module(ModuleAST),
{ok, Result} = cure_runtime:execute_module(CompiledModule).

%% Run a complete program with multiple modules
{ok, Modules} = cure_codegen:compile_program(ProgramAST),
{ok, Result} = cure_runtime:run_program(Modules).

Function Calls

State = cure_runtime:create_runtime_state(),
{ok, Result, NewState} = cure_runtime:call_function(add, [5, 3], State).

Module Loading

State = cure_runtime:create_runtime_state(),
StateWithModule = cure_runtime:load_module(CompiledModule, State).

Integration

Cure Standard Library

The runtime automatically loads and provides access to:

Result/Option monadic operations (ok, error, some, none)

List processing functions (map, filter, foldl, head, tail)

Mathematical functions (abs, sqrt, pi, safe_divide)

String operations (concat, split, trim, case conversion)

I/O functions (print, println)

FSM operations (fsm_create, fsm_send_safe)

External Function Calls

Supports calling external Erlang functions with automatic error handling and result propagation back to the Cure execution environment.

Monadic Pipe Operations

Native support for Cure's monadic pipe operator (|>) with automatic ok/error unwrapping and error propagation through cure_std:pipe/2.

Error Handling

Error Types

{function_not_found, FuncName} - Function resolution failures

{external_function_error, Error, Reason} - External function call errors

{function_execution_error, FuncName, Reason} - Internal function errors

{parameter_not_found, ParamName} - Parameter binding errors

{local_variable_not_found, VarName} - Local variable access errors

stack_underflow - Insufficient stack items for operation

{unsupported_instruction, Instruction} - Unknown instruction types

{label_not_found, Label} - Jump target resolution failures

Error Propagation

Errors are propagated through the call stack with detailed context information including function names, instruction details, and stack state.

Performance Characteristics

Instruction Execution: O(1) for most instructions

Function Resolution: O(1) hash map lookup

Stack Operations: O(1) for push/pop, O(n) for multi-item operations

Module Loading: O(n) where n is the number of functions

Memory Usage: Linear in program size and call stack depth

Thread Safety

The runtime state is designed for single-threaded execution within a process. Concurrent execution requires separate runtime state instances per thread. External function calls may interact with concurrent Erlang processes safely.

Summary

Functions

call_function(FuncName, Args, State)

Calls a function by name with the provided arguments.

create_runtime_state()

Creates a fresh runtime state with pre-loaded standard library functions.

execute_function(FuncName, Args, State)

execute_module(CompiledModule)

Executes a compiled Cure module by running its main/0 function.

load_module(CompiledModule, State)

Loads a compiled module into the runtime state, making its functions available.

record_field/2

Accesses a field from a record/tuple at runtime.

run_program/1

Runs a complete Cure program consisting of multiple modules.

Functions

call_function(FuncName, Args, State)

Calls a function by name with the provided arguments.

This is the primary interface for invoking functions within the runtime. It handles both internal Cure functions and external Erlang functions, with automatic error handling and state management.

Arguments

FuncName - Function name (atom)

Args - List of arguments to pass to the function

State - Current runtime state

Returns

{ok, Result, NewState} - Function executed successfully

{error, {function_not_found, FuncName}} - Function not in registry

{error, {external_function_error, Error, Reason}} - External function failed

{error, {function_execution_error, FuncName, Reason}} - Internal function failed

Example

State = cure_runtime:create_runtime_state(),

%% Call standard library function
{ok, Result, State1} = cure_runtime:call_function(abs, [-5], State),
%% Result = 5

%% Call user-defined function (after loading module)
StateWithModule = cure_runtime:load_module(CompiledModule, State1),
{ok, UserResult, State2} = cure_runtime:call_function(my_func, [1, 2], StateWithModule).

Function Types

External Functions

Implemented in Erlang modules (typically cure_std)

Called using apply/3 with automatic error catching

Standard library functions like print, map, abs, etc.

Maintain no internal state between calls

Internal Functions

Implemented in Cure with compiled BEAM instructions

Execute within isolated parameter/local variable scope

Can call other internal or external functions

Maintain stack-based execution model

Error Handling

Function resolution failures are reported with function name

External function errors include original Erlang error details

Internal function errors include execution context and stack trace

State is preserved across failed function calls

State Management

Global state (modules, globals) is preserved across calls

Function parameters and locals are isolated per call

Stack is managed automatically during execution

External functions cannot modify runtime state

create_runtime_state()

Creates a fresh runtime state with pre-loaded standard library functions.

This function initializes the runtime environment with all necessary components for executing Cure programs, including the complete standard library function registry.

Returns

#runtime_state{} - Fresh runtime state ready for execution

Example

State = cure_runtime:create_runtime_state(),
{ok, Result, NewState} = cure_runtime:call_function(print, ["Hello"], State).

Pre-loaded Functions

The runtime state includes immediate access to:

Monadic Operations

ok/1, error/1 - Result type constructors

some/1, none/0 - Option type constructors

map_ok/2, pipe/2 - Monadic operations

List Processing

map/2, filter/2, foldl/3 - Higher-order list functions

head/1, tail/1, length/1 - Basic list operations

find/2 - List searching

Mathematical Functions

abs/1, sqrt/1, pi/0 - Basic math

safe_divide/2, safe_sqrt/2 - Safe math operations

gcd/2, factorial/1 - Extended math functions

String Operations

string_concat/2, split/2, trim/1 - String manipulation

to_upper/1, to_lower/1 - Case conversion

contains/2, starts_with/2, ends_with/2 - String testing

string_join/2, string_empty/1 - String utilities

I/O Functions

print/1, println/1 - Console output

int_to_string/1, float_to_string/1 - Type conversion

FSM Operations

fsm_create/2, fsm_send_safe/2 - FSM management

create_counter/1 - Counter FSM creation

Function Resolution

All pre-loaded functions use external references to cure_std module functions, ensuring consistent behavior and implementation.

execute_function(FuncName, Args, State)

execute_module(CompiledModule)

Executes a compiled Cure module by running its main/0 function.

This is the primary entry point for executing standalone Cure modules. It creates a fresh runtime state, loads the module, and executes the main function if present.

Arguments

CompiledModule - Module compiled by cure_codegen:compile_module/1,2

Returns

{ok, Result} - Successfully executed with main function result

{error, main_function_not_found} - Module has no main/0 function

{error, Reason} - Execution error during main function

Example

%% Compile and execute a module with main/0
ModuleAST = parse_module("def main() = 42"),
{ok, CompiledModule} = cure_codegen:compile_module(ModuleAST),
{ok, 42} = cure_runtime:execute_module(CompiledModule).

Main Function Requirements

Must be named main

Must have arity 0 (no parameters)

Should return the program's exit value or result

Will be executed in a fresh runtime environment

Runtime Environment

The execution environment includes:

Clean runtime state with empty stack

Pre-loaded standard library functions

Module functions available for internal calls

Proper error handling and propagation

load_module(CompiledModule, State)

Loads a compiled module into the runtime state, making its functions available.

This function integrates a compiled module into the runtime environment, registering all its functions in the global function registry and storing the module for future reference.

Arguments

CompiledModule - Module compiled by cure_codegen:compile_module/1,2

State - Current runtime state

Returns

#runtime_state{} - Updated runtime state with loaded module

Example

State = cure_runtime:create_runtime_state(),
{ok, Module} = cure_codegen:compile_module(ModuleAST),
StateWithModule = cure_runtime:load_module(Module, State),

%% Now module functions are available
{ok, Result, _} = cure_runtime:call_function(my_function, [args], StateWithModule).

Module Integration

Loading a module performs the following operations:

Function Registration: All module functions are added to globals

Name Resolution: Functions become callable by name from any context

Module Storage: Module definition is stored for introspection

Namespace Merging: Functions are merged with existing global functions

Function Availability

All functions in the module become globally callable

Functions shadow previously loaded functions with same name

Both exported and non-exported functions are available (no visibility restrictions)

Functions can call other functions from the same or different loaded modules

Module Format

Expected compiled module format:

#{
    name => ModuleName,
    functions => [CompiledFunction, ...],
    exports => [{FuncName, Arity}, ...],
    attributes => [...]
}

Error Handling

Module loading is designed to always succeed. Malformed modules may result in functions that cannot be executed, but loading itself will not fail.

record_field/2

Accesses a field from a record/tuple at runtime.

This function provides runtime support for field access when the record type isn't known statically during compilation. It handles both Erlang-style records (which are tuples with the record name as the first element) and plain tuples.

Arguments

Record - The record or tuple to access

FieldName - The atom name of the field to access

Returns

The value of the specified field

Raises an error if the field doesn't exist or Record is invalid

Example

%% For a record like {turnstile_payload, 'Lock', coin}
Payload = {'TurnstilePayload', 'Lock', coin},
Event = cure_runtime:record_field(Payload, event),  % Returns coin

Implementation Notes

For Erlang records (tuples with atom tag as first element), we determine field positions from the record structure

This is a temporary solution until proper type information is available during code generation

Performance: O(1) tuple element access

run_program/1

Runs a complete Cure program consisting of multiple modules.

This function loads all provided modules into the runtime and executes the first main/0 function found across all modules. This is used for multi-module Cure programs.

Arguments

Modules - List of compiled modules from cure_codegen:compile_program/1,2

Returns

{ok, Result} - Successfully executed with main function result

{error, no_modules} - Empty module list provided

{error, main_function_not_found} - No main/0 function in any module

{error, Reason} - Execution error during program execution

Example

%% Compile and run a multi-module program
ProgramAST = [Module1AST, Module2AST, MainModuleAST],
{ok, Modules} = cure_codegen:compile_program(ProgramAST),
{ok, Result} = cure_runtime:run_program(Modules).

Module Loading Order

All modules are loaded into the runtime state first

Functions from all modules become available globally

The first main/0 function found is executed

Modules are searched in the order provided

Inter-module Dependencies

Functions from all loaded modules are available to each other

No explicit import/export checking at runtime

Name conflicts resolved by load order (later modules shadow earlier ones)

cure_show_native

Native Erlang implementations of Show trait functions for Cure.

Provides efficient primitive-to-string conversions for the Show trait system.

Summary

Functions

atom_to_string(Atom)

Convert an atom to its string representation.

bool_to_string/1

Convert a boolean to its string representation.

escape_string(Str)

Escape special characters in a string and wrap in quotes.

float_to_string(Float)

Convert a float to its string representation.

int_to_string(Int)

Convert an integer to its string representation.

is_atom_value(Val)

Check if value is an atom (for Cure pattern guards).

is_bool_value/1

Check if value is a boolean (for Cure pattern guards).

is_float_value(Val)

Check if value is a float (for Cure pattern guards).

is_integer_value(Val)

Check if value is an integer (for Cure pattern guards).

is_list_value(Val)

Check if value is a list (for Cure pattern guards).

is_string_value(Val)

Check if value is a string/binary (for Cure pattern guards).

is_tuple_value(Val)

Check if value is a tuple (for Cure pattern guards).

show_list/1

Convert a list to its string representation.

show_list_elements/1

Convert list elements to comma-separated string representations.

show_tuple/1

Convert a tuple to its string representation. Only handles tuples up to size 5 for now.

Functions

atom_to_string(Atom)

-spec atom_to_string(atom()) -> binary().

Convert an atom to its string representation.

bool_to_string/1

-spec bool_to_string(boolean()) -> binary().

Convert a boolean to its string representation.

escape_string(Str)

-spec escape_string(binary()) -> binary().

Escape special characters in a string and wrap in quotes.

float_to_string(Float)

-spec float_to_string(float()) -> binary().

Convert a float to its string representation.

int_to_string(Int)

-spec int_to_string(integer()) -> binary().

Convert an integer to its string representation.

is_atom_value(Val)

-spec is_atom_value(term()) -> boolean().

Check if value is an atom (for Cure pattern guards).

is_bool_value/1

-spec is_bool_value(term()) -> boolean().

Check if value is a boolean (for Cure pattern guards).

is_float_value(Val)

-spec is_float_value(term()) -> boolean().

Check if value is a float (for Cure pattern guards).

is_integer_value(Val)

-spec is_integer_value(term()) -> boolean().

Check if value is an integer (for Cure pattern guards).

is_list_value(Val)

-spec is_list_value(term()) -> boolean().

Check if value is a list (for Cure pattern guards).

is_string_value(Val)

-spec is_string_value(term()) -> boolean().

Check if value is a string/binary (for Cure pattern guards).

is_tuple_value(Val)

-spec is_tuple_value(term()) -> boolean().

Check if value is a tuple (for Cure pattern guards).

show_list/1

-spec show_list(list()) -> binary().

Convert a list to its string representation.

show_list_elements/1

-spec show_list_elements(list()) -> binary().

Convert list elements to comma-separated string representations.

show_tuple/1

-spec show_tuple(tuple()) -> binary().

Convert a tuple to its string representation. Only handles tuples up to size 5 for now.

cure_smt_parser

Cure SMT Model Parser

Parses S-expression output from SMT solvers (Z3, CVC5) to extract variable bindings and convert them to Erlang terms.

Features

Parse (model ...) sections

Extract (define-fun ...) statements

Convert SMT values to Erlang terms

Handle Int, Bool, Real types

Error handling for malformed output

Usage

% Parse model from Z3 output
Lines = [
    <<\"(\">>,
    <<\"  (define-fun x () Int 5)\">>,
    <<\"  (define-fun y () Int 3)\">>,
    <<\")\">>
],
{ok, Model} = cure_smt_parser:parse_model(Lines).
% => {ok, #{x => 5, y => 3}}

Summary

Functions

extract_bindings(ModelText)

Extract variable bindings from model text.

parse_define_fun(Line)

Parse a (define-fun ...) statement.

parse_model/1

Parse a model from solver output lines.

parse_value(ValueBin)

Parse a value without type information.

parse_value/2

Parse a value based on its SMT type.

Functions

extract_bindings(ModelText)

-spec extract_bindings(binary()) -> [{atom(), term()}].

Extract variable bindings from model text.

Finds all (define-fun ...) statements and extracts variable bindings.

Arguments

ModelText - Binary containing model S-expressions

Returns

List of {Name, Value} tuples

parse_define_fun(Line)

-spec parse_define_fun(binary()) -> {ok, {atom(), term()}} | {error, term()}.

Parse a (define-fun ...) statement.

Extracts variable name, type, and value from a define-fun statement.

Arguments

Line - Binary line containing define-fun

Returns

{ok, {Name, Value}} - Parsed binding

{error, Reason} - Parse error

parse_model/1

-spec parse_model([binary()]) -> {ok, map()} | {error, term()}.

Parse a model from solver output lines.

Takes a list of binary lines from the solver and extracts variable bindings.

Arguments

Lines - List of binary lines from solver output

Returns

{ok, Model} - Map of variable names to values

{error, Reason} - Parse error

Example

Lines = [<<\"(\">>, <<\"  (define-fun x () Int 5)\">>, <<\")\">>],
{ok, #{x => 5}} = parse_model(Lines).

parse_value(ValueBin)

-spec parse_value(binary()) -> term().

Parse a value without type information.

Attempts to infer type and parse accordingly.

Arguments

ValueBin - Binary containing the value

Returns

Erlang term (guessed type)

parse_value/2

-spec parse_value(atom(), binary()) -> term().

Parse a value based on its SMT type.

Converts SMT-LIB value representation to Erlang term.

Arguments

Type - SMT type atom ('Int', 'Bool', 'Real')

ValueBin - Binary containing the value

Returns

Erlang term (integer, boolean, float)

cure_smt_process

Cure SMT Solver Process Manager

Manages external SMT solver processes (Z3, CVC5) using Erlang ports. Provides process pooling, timeout enforcement, and resource management.

Features

Port-based communication with solvers

Process pool for performance

Timeout enforcement

Automatic crash recovery

Resource limits

Query execution with model extraction

Usage

% Start a solver
{ok, Pid} = cure_smt_process:start_solver(z3, 5000).

% Execute a query
Query = \"(set-logic QF_LIA)\\n(check-sat)\\n\",
{sat, Lines} = cure_smt_process:execute_query(Pid, Query).

% Stop solver
cure_smt_process:stop_solver(Pid).

Summary

Functions

code_change(OldVsn, State, Extra)

execute_query(Pid, Query)

Execute an SMT-LIB query on a solver process.

execute_query(Pid, Query, Timeout)

get_pooled_solver(PoolPid, Solver)

Get a solver from the pool.

get_stats(Pid)

Get solver statistics.

handle_call/3

handle_cast/2

handle_info/2

init/1

reset_solver(Pid)

Reset a solver process (clear all assertions).

return_solver(PoolPid, SolverPid)

Return a solver to the pool.

start_pool(Opts)

Start a solver process pool.

start_solver(Solver, Timeout)

Start a solver process.

start_solver(Solver, Timeout, Opts)

stop_pool(Pid)

Stop the solver pool.

stop_solver(Pid)

Stop a solver process.

terminate/2

Functions

code_change(OldVsn, State, Extra)

execute_query(Pid, Query)

-spec execute_query(pid(), iolist()) -> {sat | unsat | unknown, [binary()]} | {error, term()}.

Execute an SMT-LIB query on a solver process.

Arguments

Pid - Solver process PID

Query - SMT-LIB query string or iolist

Returns

{sat, Lines} - Satisfiable with model lines

{unsat, []} - Unsatisfiable

{unknown, []} - Solver couldn't determine

{error, Reason} - Execution error

execute_query(Pid, Query, Timeout)

-spec execute_query(pid(), iolist(), timeout()) -> {sat | unsat | unknown, [binary()]} | {error, term()}.

get_pooled_solver(PoolPid, Solver)

-spec get_pooled_solver(pid(), z3 | cvc5) -> {ok, pid()} | {error, term()}.

Get a solver from the pool.

get_stats(Pid)

-spec get_stats(pid()) -> map().

Get solver statistics.

handle_call/3

handle_cast/2

handle_info/2

init/1

reset_solver(Pid)

-spec reset_solver(pid()) -> ok | {error, term()}.

Reset a solver process (clear all assertions).

return_solver(PoolPid, SolverPid)

-spec return_solver(pid(), pid()) -> ok.

Return a solver to the pool.

start_pool(Opts)

-spec start_pool(map()) -> {ok, pid()}.

Start a solver process pool.

start_solver(Solver, Timeout)

-spec start_solver(z3 | cvc5, integer()) -> {ok, pid()} | {error, term()}.

Start a solver process.

Arguments

Solver - Solver type (z3 or cvc5)

Timeout - Query timeout in milliseconds

Returns

{ok, Pid} - Solver process PID

{error, Reason} - Error starting solver

start_solver(Solver, Timeout, Opts)

-spec start_solver(z3 | cvc5, integer(), list()) -> {ok, pid()} | {error, term()}.

stop_pool(Pid)

-spec stop_pool(pid()) -> ok.

Stop the solver pool.

stop_solver(Pid)

-spec stop_solver(pid()) -> ok.

Stop a solver process.

terminate/2

cure_smt_solver

Cure Programming Language - SMT Solver and Proof Assistant

The SMT (Satisfiability Modulo Theories) solver provides constraint solving capabilities for Cure's dependent type system. It handles arithmetic constraints, logical reasoning, and proof generation for dependent type verification.

Features

Constraint Solving

Arithmetic Constraints: Linear and non-linear arithmetic over integers/reals

Equality Reasoning: Equality and disequality constraints

Boolean Logic: Propositional logic with AND, OR, NOT, IMPLIES

Quantified Formulas: Existential and universal quantification

Pattern Matching Support

Length Inference: Infers list length constraints from pattern matching

Structural Constraints: Handles tuple/record structure constraints

Exhaustiveness Checking: Verifies pattern match completeness

Reachability Analysis: Determines unreachable pattern branches

Proof Generation

Constructive Proofs: Generates proof terms for valid constraints

Counter-examples: Provides counter-examples for invalid constraints

Proof Verification: Checks independently generated proofs

Automated Reasoning: Combines multiple proof strategies

Dependent Type Integration

Type-level Arithmetic: Solves constraints involving type-level values

Refinement Types: Verifies refinement type predicates

Constraint Propagation: Propagates constraints through type inference

Vector Types: Handles length-indexed vectors and arrays

Core Operations

Constraint Solving

%% Create arithmetic constraints
Constraint1 = cure_smt_solver:arithmetic_constraint(X, '+', Y),
Constraint2 = cure_smt_solver:equality_constraint(Result, Z),

%% Solve constraints
case cure_smt_solver:solve_constraints([Constraint1, Constraint2]) of
    {sat, Solution} ->
        cure_utils:debug("Solution: ~p~n", [Solution]);
    unsat ->
        cure_utils:debug("No solution exists~n");
    unknown ->
        cure_utils:debug("Cannot determine satisfiability~n")
end.

Pattern Length Inference

%% Infer length constraints from list patterns
Pattern = {list_pattern, [a, b], {identifier_pattern, tail}, Location},
LengthVar = cure_smt_solver:variable_term(list_length),
Constraints = cure_smt_solver:infer_pattern_length(Pattern, LengthVar).
%% Generates: list_length = 2 + tail_length

Proof Generation

%% Prove that a constraint follows from assumptions
Assumptions = [X_greater_than_zero, Y_positive],
Goal = cure_smt_solver:arithmetic_constraint(X, '+', Y, '>', zero),

case cure_smt_solver:prove_constraint(Assumptions, Goal) of
    {proved, Proof} ->
        cure_utils:debug("Proof: ~p~n", [Proof]);
    {disproved, CounterExample} ->
        cure_utils:debug("Counter-example: ~p~n", [CounterExample]);
    unknown ->
        cure_utils:debug("Cannot prove or disprove~n")
end.

Constraint Types

Arithmetic Constraints

Linear: ax + by = c, ax + by ≤ c

Non-linear: xy = z, x² + y² ≤ r²

Modular: x ≡ y (mod m)

Divisibility: x divides y

Logical Constraints

Propositional: P ∧ Q, P ∨ Q, ¬P

Implications: P → Q, P ↔ Q

Quantified: ∀x. P(x), ∃x. P(x)

Type-level Constraints

Length Constraints: length(xs) = n

Range Constraints: 0 ≤ index < length

Dimension Constraints: Matrix(m, n) @ Matrix(n, p) = Matrix(m, p)

SMT Solver Interface

Constraint Representation

-record(smt_constraint, {
    type :: equality | inequality | arithmetic | logical,
    left :: smt_term(),
    op :: '=' | '<' | '>' | '<=' | '>=' | '/=' | '+' | '-' | '*',
    right :: smt_term(),
    location :: location()
}).

Term Representation

-record(smt_term, {
    type :: variable | constant | expression,
    value :: atom() | integer() | float() | smt_expression(),
    location :: location()
}).

Solving Strategies

Decision Procedures

Linear Arithmetic: Simplex algorithm for linear constraints

Congruence Closure: Equality reasoning with uninterpreted functions

Bit-vectors: Precise reasoning about fixed-width integers

Arrays: Theory of arrays with select/store operations

Proof Search

Resolution: Propositional resolution with conflict analysis

DPLL(T): Integration of propositional and theory reasoning

Instantiation: Quantifier instantiation with triggers

Model Construction: Building satisfying assignments

Performance Characteristics

Linear Arithmetic: Polynomial time in most practical cases

General Arithmetic: May be exponential (semi-decidable)

Propositional Logic: NP-complete but efficient SAT solvers

Quantified Formulas: Undecidable in general, heuristic-based

Integration with Type System

Dependent Types

type Vector(T, n: Nat) where n > 0
%% SMT solver verifies: n > 0

def safe_index(v: Vector(T, n), i: Int) -> T where 0 <= i < n
%% SMT solver verifies: 0 <= i < n

Refinement Types

type Positive = Int where x > 0
type Even = Int where x % 2 == 0
%% SMT solver verifies refinement predicates

Error Handling

The SMT solver provides structured error information:

Unsatisfiable Core: Minimal unsatisfiable subset of constraints

Model Generation: Concrete counter-examples for failed proofs

Timeout Handling: Graceful degradation for complex problems

Resource Limits: Configurable limits on solving time/memory

External Solver Integration

Supports integration with external SMT solvers:

Z3: Microsoft Research SMT solver

CVC4: Stanford/NYU SMT solver

Yices: SRI SMT solver

MathSAT: FBKIRST SMT solver

Thread Safety

The SMT solver is stateless and thread-safe. Multiple constraint solving operations can run concurrently without interference.

Summary

Types

location()

proof_term()

smt_constraint()

smt_expression()

smt_term()

Functions

addition_expression(Terms)

arithmetic_constraint(Left, Op, Right)

check_proof/2

check_satisfiable(Constraint)

constant_term(Value)

constraint_to_string/1

division_expression(Terms)

equality_constraint(Left, Right)

generate_proof(Assumptions, Goal)

implication_constraint(Premise, Conclusion)

inequality_constraint(Left, Op, Right)

infer_pattern_length/2

infer_pattern_length_constraint(Pattern, OriginalLengthVar)

infer_tail_length_constraint/3

list_pattern_length_constraint(Pattern, LengthVar)

modulo_expression(Terms)

multiplication_expression(Terms)

negate_constraint(Constraint)

new_constraint(Type, Op, Right)

prove_constraint(Assumptions, Goal)

solve_constraints(Constraints)

solve_constraints(Constraints, InitialAssignment)

subtraction_expression(Terms)

variable_term(Name)

Types

location()

-type location() :: #location{line :: term(), column :: term(), file :: term()}.

proof_term()

-type proof_term() ::
          #proof_term{conclusion :: smt_constraint(),
                      premises :: [smt_constraint()],
                      rule :: atom(),
                      subproofs :: [proof_term()]}.

smt_constraint()

-type smt_constraint() ::
          #smt_constraint{type :: equality | inequality | arithmetic | logical,
                          left :: smt_term(),
                          op ::
                              '=' | '<' | '>' | '<=' | '>=' | '/=' | '+' | '-' | '*' | 'and' | 'or' |
                              implies,
                          right :: smt_term(),
                          location :: location()}.

smt_expression()

-type smt_expression() ::
          #smt_expression{op :: '+' | '-' | '*' | '/' | mod,
                          args :: [smt_term()],
                          location :: location()}.

smt_term()

-type smt_term() ::
          #smt_term{type :: variable | constant | expression,
                    value :: atom() | integer() | float() | smt_expression(),
                    location :: location()}.

Functions

addition_expression(Terms)

arithmetic_constraint(Left, Op, Right)

-spec arithmetic_constraint(smt_term(), atom(), smt_term()) -> smt_constraint().

check_proof/2

check_satisfiable(Constraint)

-spec check_satisfiable(smt_constraint()) -> boolean().

constant_term(Value)

constraint_to_string/1

division_expression(Terms)

equality_constraint(Left, Right)

-spec equality_constraint(smt_term(), smt_term()) -> smt_constraint().

generate_proof(Assumptions, Goal)

implication_constraint(Premise, Conclusion)

-spec implication_constraint(smt_constraint(), smt_constraint()) -> smt_constraint().

inequality_constraint(Left, Op, Right)

infer_pattern_length/2

-spec infer_pattern_length(term(), smt_term()) -> [smt_constraint()].

infer_pattern_length_constraint(Pattern, OriginalLengthVar)

-spec infer_pattern_length_constraint(term(), atom()) -> [smt_constraint()].

infer_tail_length_constraint/3

-spec infer_tail_length_constraint(term(), atom(), atom()) -> [smt_constraint()].

list_pattern_length_constraint(Pattern, LengthVar)

-spec list_pattern_length_constraint(term(), atom()) -> smt_constraint().

modulo_expression(Terms)

multiplication_expression(Terms)

negate_constraint(Constraint)

new_constraint(Type, Op, Right)

-spec new_constraint(atom(), atom(), smt_term()) -> smt_constraint().

prove_constraint(Assumptions, Goal)

-spec prove_constraint([smt_constraint()], smt_constraint()) ->
                          {proved, proof_term()} | {disproved, proof_term()} | unknown.

solve_constraints(Constraints)

-spec solve_constraints([smt_constraint()]) -> {sat, #{atom() => term()}} | unsat | unknown.

solve_constraints(Constraints, InitialAssignment)

-spec solve_constraints([smt_constraint()], #{atom() => term()}) ->
                           {sat, #{atom() => term()}} | unsat | unknown.

subtraction_expression(Terms)

variable_term(Name)

cure_smt_translator

Cure SMT-LIB Translator

Translates Cure type constraints and expressions into SMT-LIB format for consumption by external SMT solvers (Z3, CVC5).

Features

Full translation of Cure expressions to SMT-LIB s-expressions

Type mapping (Int, Nat, Bool, Float to SMT types)

Logic inference (QF_LIA, QF_LRA, etc.)

Variable declaration generation

Assertion generation from constraints

Usage

% Translate a constraint to SMT-LIB query
Constraint = #binary_op_expr{op = '>', left = var(x), right = lit(0)},
Env = #{x => {type, int}},
Query = cure_smt_translator:generate_query(Constraint, Env).
% => \"(set-logic QF_LIA)\\n(declare-const x Int)\\n(assert (> x 0))\\n(check-sat)\\n\"

Summary

Types

expr()

smt_logic()

Functions

collect_variables(Constraint, Env)

Collect all variables from a constraint.

declare_variable(VarName, Env)

Generate SMT-LIB declaration for a variable.

generate_query(Constraint, Env)

Generate a complete SMT-LIB query from a Cure constraint.

generate_query(Constraint, Env, Opts)

Generate SMT-LIB query with options.

infer_logic(Constraint)

Infer the appropriate SMT-LIB logic for a constraint.

translate_expr(Expr)

Translate a Cure expression to SMT-LIB s-expression.

translate_expr/2

Types

expr()

-type expr() ::
          #literal_expr{value :: term(), location :: term()} |
          #identifier_expr{name :: term(), location :: term()} |
          #function_call_expr{function :: term(), args :: term(), location :: term()} |
          #match_expr{expr :: term(), patterns :: term(), location :: term()} |
          #let_expr{bindings :: term(), body :: term(), location :: term()} |
          #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} |
          #unary_op_expr{op :: term(), operand :: term(), location :: term()} |
          #list_expr{elements :: term(), location :: term()} |
          #tuple_expr{elements :: term(), location :: term()} |
          #record_expr{name :: term(), fields :: term(), location :: term()} |
          #field_access_expr{record :: term(), field :: term(), location :: term()} |
          #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} |
          #lambda_expr{params :: term(), body :: term(), location :: term()} |
          #fsm_spawn_expr{fsm_name :: term(),
                          init_args :: term(),
                          init_state :: term(),
                          location :: term()} |
          #fsm_send_expr{target :: term(), message :: term(), location :: term()} |
          #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} |
          #fsm_state_expr{location :: term()} |
          #qualified_call_expr{trait_name :: term(),
                               type_args :: term(),
                               method_name :: term(),
                               receiver :: term(),
                               args :: term(),
                               location :: term()}.

smt_logic()

-type smt_logic() :: 'QF_LIA' | 'QF_LRA' | 'QF_LIRA' | 'QF_NIA' | 'QF_NRA' | 'QF_UFLIA'.

Functions

collect_variables(Constraint, Env)

-spec collect_variables(expr(), map()) -> [atom()].

Collect all variables from a constraint.

Traverses the AST to find all variable references.

Arguments

Constraint - Cure AST expression

Env - Environment (for type information)

Returns

[atom()] - List of variable names (deduplicated)

declare_variable(VarName, Env)

-spec declare_variable(atom(), map()) -> iolist().

Generate SMT-LIB declaration for a variable.

Creates a (declare-const ...) declaration based on the variable's type.

Arguments

VarName - Variable name (atom)

Env - Environment with type information

Returns

iolist() - SMT-LIB declaration

generate_query(Constraint, Env)

-spec generate_query(expr(), map()) -> iolist().

Generate a complete SMT-LIB query from a Cure constraint.

Produces a full SMT-LIB query including logic declaration, variable declarations, assertions, and check-sat command.

Arguments

Constraint - Cure AST expression representing the constraint

Env - Environment mapping variables to types

Returns

iolist() - SMT-LIB query as iolist (use iolist_to_binary/1 to convert)

Example

Constraint = #binary_op_expr{op = '+', left = var(x), right = var(y)},
Query = generate_query(Constraint, #{x => {type, int}, y => {type, int}}).

generate_query(Constraint, Env, Opts)

-spec generate_query(expr(), map(), map()) -> iolist().

Generate SMT-LIB query with options.

Options

{get_model, boolean()} - Include (get-model) command (default: true)

{logic, smt_logic()} - Override logic inference

{timeout, integer()} - Solver timeout hint in milliseconds

infer_logic(Constraint)

-spec infer_logic(expr()) -> smt_logic().

Infer the appropriate SMT-LIB logic for a constraint.

Analyzes the constraint to determine which SMT-LIB logic is required.

Logics

QF_LIA - Quantifier-free linear integer arithmetic

QF_LRA - Quantifier-free linear real arithmetic

QF_LIRA - Quantifier-free linear integer/real arithmetic

QF_NIA - Quantifier-free nonlinear integer arithmetic

Arguments

Constraint - Cure AST expression

Returns

smt_logic() - Inferred logic

translate_expr(Expr)

-spec translate_expr(expr()) -> iolist().

Translate a Cure expression to SMT-LIB s-expression.

Converts Cure AST expressions to SMT-LIB format recursively.

Arguments

Expr - Cure AST expression

Returns

iolist() - SMT-LIB s-expression

translate_expr/2

-spec translate_expr(expr(), map()) -> iolist().

cure_std

Cure Programming Language - Standard Library Runtime

Provides core runtime functions that cannot be implemented in pure Cure due to their need for Erlang-specific features. This module contains the essential low-level operations for I/O, monadic operations, FSM integration, and value serialization.

Architecture

This module represents the boundary between pure Cure code and the underlying Erlang runtime. Most standard library functions are now implemented in Cure itself (in lib/std/), but this module contains the irreducible core that requires direct Erlang integration.

Core Responsibilities

Monadic Operations: Implementation of Result/Option pipe semantics

I/O Operations: Console output and formatting functions

FSM Integration: Bridge to FSM runtime system

Value Serialization: Converting Cure values to string representations

Runtime Utilities: Low-level operations for runtime system

Function Categories

Monadic Operations

pipe/2 - Monadic pipe operator implementation

is_monad/1 - Type checking for Result/Option values

I/O Functions

print/1 - Output without newline

println/1 - Output with newline

show/1 - Convert values to string representation

FSM Operations

fsm_create/2 - Create FSM instances

fsm_send_safe/2 - Safe message sending to FSMs

create_counter/1 - Specialized counter FSM creation

Utility Functions

list_to_string/1 - List serialization

join_ints/2 - Integer list formatting

Monadic Pipe Semantics

The pipe/2 function implements Cure's monadic pipe operator (|>) with these rules:

Error Propagation: Error(x) |> f = Error(x)

Ok Unwrapping: Ok(x) |> f = f(x) (wrapped if not already monadic)

Value Passing: x |> f = f(x) (wrapped if not already monadic)

Example Usage

%% Direct function calls (typically from runtime)
cure_std:print("Hello, World!").
cure_std:pipe({'Ok', 5}, fun(X) -> X * 2 end).
%% Returns: {'Ok', 10}

cure_std:show({'Ok', [1, 2, 3]}).
%% Returns: "Ok([1, 2, 3])"

Integration with Cure

Functions in this module are automatically registered in the runtime's global function registry and can be called from Cure code using standard function call syntax. The runtime handles the bridge between Cure's type system and Erlang's dynamic typing.

Error Handling

I/O functions always succeed (return 'ok')

Pipe operations catch Erlang exceptions and wrap them as Error values

FSM operations return Result types for safe error handling

Show function handles unknown types gracefully

Performance Considerations

All functions are designed for single-call efficiency

String operations use efficient list concatenation

Monadic operations minimize pattern matching overhead

FSM operations are lightweight stubs (full implementation in cure_fsm_runtime)

Summary

Functions

create_counter(InitialValue)

fsm_create(FSMType, InitialState)

fsm_send_safe(FSMRef, Message)

is_monad/1

Checks if a value is a monadic type (Result or Option).

join_ints/2

list_to_string(List)

pipe/2

Implements Cure's monadic pipe operator (|>) with Result type semantics.

print(Message)

Prints a message to standard output without adding a newline.

println(Message)

Prints a message to standard output followed by a newline.

'Succ'(N)

Nat type unary constructor representing successor.

show/1

Converts any Cure value to its string representation for debugging and display.

'Zero'()

Nat type nullary constructor representing zero.

Functions

create_counter(InitialValue)

fsm_create(FSMType, InitialState)

fsm_send_safe(FSMRef, Message)

is_monad/1

Checks if a value is a monadic type (Result or Option).

This function determines whether a value follows the monadic pattern used by Cure's Result and Option types, which is essential for proper pipe operator behavior.

Arguments

Value - Any Erlang term to check

Returns

true - Value is a Result (Ok/Error) type

false - Value is not a monadic type

Example

cure_std:is_monad({'Ok', 42}).     %% true
cure_std:is_monad({'Error', msg}). %% true
cure_std:is_monad(42).             %% false
cure_std:is_monad([1, 2, 3]).      %% false

Supported Monadic Types

{'Ok', Value} - Successful result with value

{'Error', Reason} - Failed result with error reason

Note: Option types (Some/None) are not currently detected as monadic by this function, though they follow similar patterns.

Usage

Primarily used internally by pipe/2 to determine whether function results need to be wrapped in Ok constructors or can be returned as-is.

join_ints/2

list_to_string(List)

pipe/2

Implements Cure's monadic pipe operator (|>) with Result type semantics.

This function is the core implementation of Cure's pipe operator, providing monadic composition with automatic error propagation and value wrapping. It handles three distinct cases based on the input value type.

Arguments

LHO - Left-hand operand (value to be piped)

RHO - Right-hand operand (function to apply)

Returns

Result of applying RHO to LHO (possibly unwrapped), with appropriate wrapping

Error values are propagated without calling RHO

Runtime errors are caught and wrapped as Error values

Pipe Rules

Rule 1: Error Propagation

cure_std:pipe({'Error', reason}, Fun).
%% Returns: {'Error', reason} (Fun is not called)

Rule 2: Ok Unwrapping

cure_std:pipe({'Ok', 5}, fun(X) -> X * 2 end).
%% Returns: {'Ok', 10} (value unwrapped, result wrapped)

cure_std:pipe({'Ok', 5}, fun(X) -> {'Ok', X * 2} end).
%% Returns: {'Ok', 10} (already monadic, not double-wrapped)

Rule 3: Value Passing

cure_std:pipe(5, fun(X) -> X * 2 end).
%% Returns: {'Ok', 10} (non-monadic input, result wrapped)

cure_std:pipe(5, fun(X) -> {'Error', 'too_big'} end).
%% Returns: {'Error', 'too_big'} (monadic result preserved)

Error Handling

If RHO throws an exception during execution:

cure_std:pipe({'Ok', 0}, fun(X) -> 1/X end).
%% Returns: {'Error', {pipe_runtime_error, error, badarith}}

Usage in Cure

%% In Cure code, this becomes:
value |> function1 |> function2

%% Which compiles to:
pipe(pipe(value, function1), function2)

Type Safety

The pipe operator maintains type safety by:

Never double-wrapping already monadic values

Propagating errors without execution

Catching runtime exceptions as Error values

Preserving monadic invariants through composition chains

print(Message)

Prints a message to standard output without adding a newline.

This function outputs text directly to the console using Erlang's I/O formatting system. It's designed for inline output where you want to continue writing on the same line.

Arguments

Message - String or list to print (must be printable)

Returns

ok - Always succeeds

Example

cure_std:print("Hello ").
cure_std:print("World!").
%% Output: "Hello World!"

cure_std:print("Count: ").
cure_std:print(integer_to_list(42)).
%% Output: "Count: 42"

Usage in Cure

print("Processing...")
// Continue with other operations
print("Done!")

Character Encoding

Supports Unicode text through Erlang's ~ts format specifier, ensuring proper handling of international characters.

Error Handling

I/O errors are handled by the underlying Erlang system. This function always returns 'ok' from the Cure perspective.

println(Message)

Prints a message to standard output followed by a newline.

This is the most commonly used output function, automatically adding a newline character after the message for line-by-line output formatting.

Arguments

Message - String or list to print (must be printable)

Returns

ok - Always succeeds

Example

cure_std:println("First line").
cure_std:println("Second line").
%% Output:
%% First line
%% Second line

cure_std:println("Value: " ++ integer_to_list(42)).
%% Output: Value: 42

Usage in Cure

println("Hello, World!")
println("This is on a new line")

Character Encoding

Supports Unicode text through Erlang's ~ts format specifier, ensuring proper handling of international characters.

Comparison with print/1

print/1 - No newline, for inline output

println/1 - Adds newline, for line-based output

Error Handling

I/O errors are handled by the underlying Erlang system. This function always returns 'ok' from the Cure perspective.

'Succ'(N)

Nat type unary constructor representing successor.

Takes a natural number and returns its successor (n+1). This is the inductive case of Peano-encoded natural numbers.

Arguments

N - A natural number (Nat)

Returns

N+1 (next natural number)

Example

cure_std:'Succ'(0).        %% Returns: 1 (successor of Zero)
cure_std:'Succ'(5).        %% Returns: 6 (successor of 5)

Usage in Cure

let one = Succ(Zero)
let two = Succ(Succ(Zero))
let three = Succ(two)

Type

Succ : Nat -> Nat

show/1

Converts any Cure value to its string representation for debugging and display.

This function provides comprehensive string serialization for all Cure data types, with special handling for monadic types (Result/Option) and structured data like lists and tuples.

Arguments

Value - Any Cure/Erlang term to convert to string

Returns

String representation of the value

"unknown" for unrecognized value types

Examples

Monadic Types

cure_std:show({'Ok', 42}).        %% "Ok(42)"
cure_std:show({'Error', failed}). %% "Error(failed)"
cure_std:show({'Some', data}).    %% "Some(data)"
cure_std:show('None').            %% "None"

Basic Types

cure_std:show(42).           %% "42"
cure_std:show(3.14).         %% "3.14"
cure_std:show(hello).        %% "hello"
cure_std:show("string").     %% "string"

Structured Types

cure_std:show([1, 2, 3]).           %% "[1, 2, 3]"
cure_std:show({a, b}).              %% "{a, b}"
cure_std:show({1, 2, 3, 4}).        %% "{1, 2, 3, 4}"
cure_std:show({1, 2, 3, 4, 5}).     %% "{1, 2, 3, 4, ...}"

Nested Structures

cure_std:show({'Ok', [1, 2, {'Some', 3}]}).
%% "Ok([1, 2, Some(3)])"

Usage in Cure

let value = Ok([1, 2, 3])
println(show(value))  // Outputs: Ok([1, 2, 3])

Tuple Handling

Tuples with 0-4 elements: Full representation

Tuples with 5+ elements: Truncated with "..." suffix

Nested tuples are recursively formatted

Error Handling

Unknown or unsupported types return "unknown" rather than crashing, making this function safe for debugging any Cure value.

Performance Notes

Recursive formatting for nested structures

String concatenation using Erlang's efficient list operations

Optimized for readability over performance

'Zero'()

Nat type nullary constructor representing zero.

In Cure's Peano encoding of natural numbers:

Zero represents 0

Succ(Zero) represents 1

Succ(Succ(Zero)) represents 2, etc.

Returns

0 (represented as integer for runtime efficiency)

Example

cure_std:'Zero'().  %% Returns: 0

Usage in Cure

def length(list: List(T)): Nat =
  match list do
    [] -> Zero
    [_ | t] -> Succ(length(t))
  end

Type

Zero : Nat

cure_string_native

Native Erlang implementations of string operations for Cure.

Provides high-performance string manipulation functions that operate on UTF-8 binaries (String type) and charlists (Charlist type).

Summary

Functions

at(String, Index)

Get the grapheme at a specific index (0-based). Returns {ok, Grapheme} or {error, out_of_bounds}.

byte_size(String)

Get the byte size of a string.

capitalize/1

Capitalize the first grapheme of a string.

codepoints(String)

Get a list of Unicode codepoints from a string.

concat(S1, S2)

Concatenate two strings efficiently.

contains(String, Substring)

Check if a string contains a substring.

downcase(String)

Convert string to lowercase (Unicode-aware).

duplicate(String, N)

Duplicate a string n times.

ends_with(String, Suffix)

Check if a string ends with a given suffix.

first/1

Get the first grapheme of a string.

from_binary(Bin)

Convert a binary to a string, validating UTF-8. Returns {ok, String} or {error, invalid_utf8}.

from_charlist(Charlist)

Convert a charlist to a UTF-8 string.

graphemes(String)

Split a string into a list of grapheme clusters.

is_empty/1

Check if a string is empty.

join/2

Join a list of strings with a separator.

last/1

Get the last grapheme of a string.

length(String)

Get the length of a string in graphemes (Unicode-aware).

pad_left(String, Width, Padding)

Pad a string on the left to a given width.

pad_right(String, Width, Padding)

Pad a string on the right to a given width.

replace(String, Pattern, Replacement)

Replace the first occurrence of a pattern.

replace_all(String, Pattern, Replacement)

Replace all occurrences of a pattern.

reverse(String)

Reverse a string (Unicode-aware, reverses graphemes).

slice(String, Start, Length)

Extract a substring by grapheme position and length.

split(String, Pattern)

Split a string by a pattern.

split_at(String, Index)

Split a string at a specific grapheme index.

starts_with(String, Prefix)

Check if a string starts with a given prefix.

to_atom(String)

Convert string to atom.

to_binary(String)

Convert string to raw binary (identity function for strings).

to_charlist(String)

Convert a UTF-8 string to a charlist.

trim(String)

Trim whitespace from both ends of a string.

trim_left(String)

Trim whitespace from the left side of a string.

trim_right(String)

Trim whitespace from the right side of a string.

upcase(String)

Convert string to uppercase (Unicode-aware).

valid_utf8(Bin)

Check if a binary is valid UTF-8.

Functions

at(String, Index)

-spec at(binary(), integer()) -> {ok, binary()} | {error, atom()}.

Get the grapheme at a specific index (0-based). Returns {ok, Grapheme} or {error, out_of_bounds}.

byte_size(String)

-spec byte_size(binary()) -> non_neg_integer().

Get the byte size of a string.

capitalize/1

-spec capitalize(binary()) -> binary().

Capitalize the first grapheme of a string.

codepoints(String)

-spec codepoints(binary()) -> [integer()].

Get a list of Unicode codepoints from a string.

concat(S1, S2)

-spec concat(binary(), binary()) -> binary().

Concatenate two strings efficiently.

contains(String, Substring)

-spec contains(binary(), binary()) -> boolean().

Check if a string contains a substring.

downcase(String)

-spec downcase(binary()) -> binary().

Convert string to lowercase (Unicode-aware).

duplicate(String, N)

-spec duplicate(binary(), non_neg_integer()) -> binary().

Duplicate a string n times.

ends_with(String, Suffix)

-spec ends_with(binary(), binary()) -> boolean().

Check if a string ends with a given suffix.

first/1

-spec first(binary()) -> {ok, binary()} | {error, atom()}.

Get the first grapheme of a string.

from_binary(Bin)

-spec from_binary(binary()) -> {ok, binary()} | {error, atom()}.

Convert a binary to a string, validating UTF-8. Returns {ok, String} or {error, invalid_utf8}.

from_charlist(Charlist)

-spec from_charlist(list()) -> binary().

Convert a charlist to a UTF-8 string.

graphemes(String)

-spec graphemes(binary()) -> [binary()].

Split a string into a list of grapheme clusters.

is_empty/1

-spec is_empty(binary()) -> boolean().

Check if a string is empty.

join/2

-spec join([binary()], binary()) -> binary().

Join a list of strings with a separator.

last/1

-spec last(binary()) -> {ok, binary()} | {error, atom()}.

Get the last grapheme of a string.

length(String)

-spec length(binary()) -> non_neg_integer().

Get the length of a string in graphemes (Unicode-aware).

pad_left(String, Width, Padding)

-spec pad_left(binary(), non_neg_integer(), binary()) -> binary().

Pad a string on the left to a given width.

pad_right(String, Width, Padding)

-spec pad_right(binary(), non_neg_integer(), binary()) -> binary().

Pad a string on the right to a given width.

replace(String, Pattern, Replacement)

-spec replace(binary(), binary(), binary()) -> binary().

Replace the first occurrence of a pattern.

replace_all(String, Pattern, Replacement)

-spec replace_all(binary(), binary(), binary()) -> binary().

Replace all occurrences of a pattern.

reverse(String)

-spec reverse(binary()) -> binary().

Reverse a string (Unicode-aware, reverses graphemes).

slice(String, Start, Length)

-spec slice(binary(), integer(), non_neg_integer()) -> binary().

Extract a substring by grapheme position and length.

split(String, Pattern)

-spec split(binary(), binary()) -> [binary()].

Split a string by a pattern.

split_at(String, Index)

-spec split_at(binary(), integer()) -> {binary(), binary()}.

Split a string at a specific grapheme index.

starts_with(String, Prefix)

-spec starts_with(binary(), binary()) -> boolean().

Check if a string starts with a given prefix.

to_atom(String)

-spec to_atom(binary()) -> atom().

Convert string to atom.

to_binary(String)

-spec to_binary(binary()) -> binary().

Convert string to raw binary (identity function for strings).

to_charlist(String)

-spec to_charlist(binary()) -> list().

Convert a UTF-8 string to a charlist.

trim(String)

-spec trim(binary()) -> binary().

Trim whitespace from both ends of a string.

trim_left(String)

-spec trim_left(binary()) -> binary().

Trim whitespace from the left side of a string.

trim_right(String)

-spec trim_right(binary()) -> binary().

Trim whitespace from the right side of a string.

upcase(String)

-spec upcase(binary()) -> binary().

Convert string to uppercase (Unicode-aware).

valid_utf8(Bin)

-spec valid_utf8(binary()) -> boolean().

Check if a binary is valid UTF-8.

cure_type_optimizer

Cure Programming Language - Type-directed Optimizer

The type optimizer leverages rich type information from Cure's dependent type system to perform sophisticated program optimizations. It analyzes type usage patterns, specializes generic functions, eliminates dead code, and optimizes memory layouts based on static type analysis.

Key Features

Function Specialization

Type-based Specialization: Creates specialized versions of generic functions

Call-site Analysis: Identifies frequent type instantiations

Cost-benefit Analysis: Balances code size vs. performance gains

Automatic Generation: Generates specialized function variants

Monomorphization

Generic Elimination: Converts polymorphic functions to monomorphic variants

Type Instantiation: Resolves all type variables with concrete types

Dispatch Optimization: Eliminates runtime type dispatch overhead

Template Expansion: Expands type templates at compile time

Inlining Optimization

Type-guided Inlining: Uses type information for better inlining decisions

Call-site Specialization: Inlines based on argument types

Size Thresholds: Configurable limits to prevent code bloat

Hot-path Optimization: Prioritizes frequently executed code paths

Dead Code Elimination

Type-based Reachability: Uses type analysis for precise dead code detection

Specialization Cleanup: Removes unused specialized variants

Constraint-based Analysis: Leverages dependent type constraints

Whole-program Analysis: Global dead code elimination

Memory Layout Optimization

Struct Packing: Optimizes memory layout based on type information

Cache-aware Layouts: Arranges fields for better cache locality

Alignment Optimization: Ensures proper alignment for performance

Size Minimization: Reduces memory footprint where possible

Optimization Pipeline

Phase 1: Type Analysis

{TypeInfo, UsageStats} = cure_type_optimizer:analyze_program_types(AST),
%% Collects:
%% - Function type signatures
%% - Call site information with argument types
%% - Type usage frequencies
%% - Monomorphic instantiation opportunities

Phase 2: Opportunity Identification

Context = cure_type_optimizer:find_optimization_opportunities(AST, Context1),
%% Identifies:
%% - Specialization candidates
%% - Inlining opportunities
%% - Dead code
%% - Memory layout improvements

Phase 3: Optimization Application

OptimizedAST = cure_type_optimizer:run_optimization_passes(AST, Context2),
%% Applies optimizations in order:
%% 1. Function specialization
%% 2. Monomorphization
%% 3. Inlining
%% 4. Dead code elimination
%% 5. Memory layout optimization

Usage Examples

Program Optimization

%% Basic optimization with default settings
{ok, OptimizedAST, Report} = cure_type_optimizer:optimize_program(AST),

%% Custom optimization configuration
Config = #optimization_config{
    level = 3,  % Aggressive optimization
    enable_specialization = true,
    max_specializations = 20,
    inline_threshold = 100
},
{ok, OptimizedAST, Report} = cure_type_optimizer:optimize_program(AST, Config).

Module-level Optimization

{ok, OptimizedModule} = cure_type_optimizer:optimize_module(Module),

%% With custom config
{ok, OptimizedModule} = cure_type_optimizer:optimize_module(Module, Config).

Individual Optimization Passes

%% Run specific optimization passes
SpecializedAST = cure_type_optimizer:function_specialization_pass(AST),
MonomorphicAST = cure_type_optimizer:monomorphization_pass(SpecializedAST),
InlinedAST = cure_type_optimizer:inlining_pass(MonomorphicAST).

Configuration Options

Optimization Levels

Level 0: No optimizations (debugging)

Level 1: Basic optimizations (safe, minimal)

Level 2: Standard optimizations (default, balanced)

Level 3: Aggressive optimizations (maximum performance)

Fine-grained Control

Specialization Limits: Maximum number of specialized variants

Inlining Thresholds: Size limits for function inlining

Memory Optimization: Enable/disable layout optimizations

Pass Selection: Enable/disable individual optimization passes

Performance Characteristics

Typical Improvements

Function Calls: 25-60% improvement through specialization

Memory Usage: 10-30% reduction through layout optimization

Code Size: Variable (may increase with specialization, decrease with DCE)

Compile Time: Increases proportionally to optimization level

Analysis Complexity

Type Analysis: O(n log n) where n is program size

Specialization: O(k × m) where k is candidates, m is instantiations

Dead Code: O(n + e) where e is call graph edges

Memory Layout: O(t) where t is number of types

Integration

The type optimizer integrates with:

Type Checker: Uses inferred type information

Code Generator: Provides optimized AST for compilation

Runtime: Optimizes for runtime performance characteristics

Profiler: Can use runtime profiling data for optimization hints

Optimization Report

Generates detailed reports including:

Specializations Created: List of generated specialized functions

Inlining Decisions: Functions inlined and their sizes

Dead Code Eliminated: Removed functions and their impact

Memory Improvements: Layout changes and size reductions

Performance Estimates: Expected performance improvements

Safety and Correctness

Type Preservation: All optimizations preserve type safety

Semantic Equivalence: Optimized code maintains original semantics

Constraint Preservation: Dependent type constraints are maintained

Error Handling: Graceful degradation when optimization fails

Summary

Functions

analyze_program_types(AST)

analyze_specialization_candidates(AST)

analyze_type_usage(AST)

collect_call_sites/1

collect_poly_instantiation_sites/1

collect_poly_instantiations_from_expr/2

collect_poly_instantiations_from_function/1

collect_poly_instantiations_from_module/1

collect_type_information(AST)

collect_type_usage_patterns/1

count_function_calls/1

create_monomorphic_function/3

dead_code_elimination_pass(AST)

dead_code_elimination_pass(AST, Context)

default_optimization_config()

eliminate_unused_specializations/2

find_optimization_opportunities(AST, Context)

find_reachable_functions(AST, EntryPoints)

find_specialization_opportunities(AST)

function_specialization_pass(AST)

function_specialization_pass(AST, Context)

generate_specialized_variants(AST, InstantiationSites)

identify_cold_code(AST)

identify_hot_paths(AST)

initialize_optimization_context(Config)

inlining_pass(AST)

inlining_pass(AST, Context)

memory_layout_optimization_pass(AST)

memory_layout_optimization_pass(AST, Context)

monomorphization_pass(AST)

monomorphization_pass(AST, Context)

monomorphize_ast/2

optimize_module(Module)

optimize_module(Module, Config)

optimize_program(AST)

optimize_program(AST, Config)

replace_poly_calls_in_expr/2

run_optimization_passes(AST, Context)

set_optimization_level(Level)

specialize_function_body(Body, TypeSubst, OrigFuncName)

track_polymorphic_call(FuncName, Args, Location)

transform_ast_with_specializations/2

Functions

analyze_program_types(AST)

analyze_specialization_candidates(AST)

analyze_type_usage(AST)

collect_call_sites/1

collect_poly_instantiation_sites/1

collect_poly_instantiations_from_expr/2

collect_poly_instantiations_from_function/1

collect_poly_instantiations_from_module/1

collect_type_information(AST)

collect_type_usage_patterns/1

count_function_calls/1

create_monomorphic_function/3

dead_code_elimination_pass(AST)

dead_code_elimination_pass(AST, Context)

default_optimization_config()

eliminate_unused_specializations/2

find_optimization_opportunities(AST, Context)

find_reachable_functions(AST, EntryPoints)

find_specialization_opportunities(AST)

function_specialization_pass(AST)

function_specialization_pass(AST, Context)

generate_specialized_variants(AST, InstantiationSites)

identify_cold_code(AST)

identify_hot_paths(AST)

initialize_optimization_context(Config)

inlining_pass(AST)

inlining_pass(AST, Context)

memory_layout_optimization_pass(AST)

memory_layout_optimization_pass(AST, Context)

monomorphization_pass(AST)

monomorphization_pass(AST, Context)

monomorphize_ast/2

optimize_module(Module)

optimize_module(Module, Config)

optimize_program(AST)

optimize_program(AST, Config)

replace_poly_calls_in_expr/2

run_optimization_passes(AST, Context)

set_optimization_level(Level)

specialize_function_body(Body, TypeSubst, OrigFuncName)

track_polymorphic_call(FuncName, Args, Location)

transform_ast_with_specializations/2

cure_typechecker

Cure Programming Language - Type Checker

The type checker module provides high-level type checking functionality for Cure programs. It works with parsed AST nodes and implements comprehensive static type analysis including dependent type verification, constraint solving, and type inference.

Features

Comprehensive Type Checking

Program-Level Analysis: Full program type checking with module support

Function Type Checking: Parameter and return type verification

Expression Type Inference: Bottom-up type inference for all expressions

Dependent Type Support: Verification of dependent type constraints

Module System Support

Module Scoping: Proper scoping of types and functions within modules

Export Verification: Ensures exported functions exist and have correct types

Import Resolution: Type-safe import of functions and types from other modules

Two-Pass Processing: Collects signatures before checking bodies

Advanced Type Features

Generic Functions: Full support for parametric polymorphism

Constraint Solving: Integration with SMT-based constraint solving

FSM Type Checking: Verification of finite state machine definitions

Erlang Interop: Type checking for Erlang function interfaces

Error Reporting

Detailed Error Messages: Precise error locations with helpful descriptions

Warning System: Non-fatal issues that may indicate problems

Error Recovery: Continues checking after errors to find more issues

Structured Results: Machine-readable error and warning information

Type Checking Process

1. Environment Setup

Env = cure_typechecker:builtin_env(),  % Built-in types and functions
R esult = cure_typechecker:check_program(AST).

2. Module Processing

Signature Collection: First pass collects all function signatures

Body Checking: Second pass verifies function bodies against signatures

Export Validation: Ensures all exported items are properly typed

3. Function Analysis

Parameter Processing: Converts parameter types to environment bindings

Constraint Checking: Verifies function constraints are boolean expressions

Body Inference: Infers body type and checks against declared return type

Generic Resolution: Resolves type parameters and constraints

Usage Examples

Program Type Checking

AST = cure_parser:parse_file("example.cure"),
Result = cure_typechecker:check_program(AST),
case Result#typecheck_result.success of
  true ->
    cure_utils:debug("Type checking successful~n");

  false ->
    Errors = Result#typecheck_result.errors,
    cure_utils:debug("Type errors: ~p~n", [Errors])
end.

Function Type Checking

FuncAST = #function_def{name = add, params = Params, body = Body, ...},
{ok, Env, Result} = cure_typechecker:check_function(FuncAST).

Expression Type Inference

{ok, Type} = cure_typechecker:check_expression(ExprAST, Environment).

Type Checking Results

Returns structured results with:

Success Flag: Overall type checking success/failure

Inferred Types: Types inferred for expressions and functions

Error List: Detailed error information with locations

Warnings: Non-fatal issues found during checking

Built-in Environment

Provides built-in types and functions:

Primitive Types: Int, Float, String, Bool, Atom

Type Constructors: List, Tuple, Map, Vector

Standard Functions: Arithmetic, logical, and utility functions

FSM Operations: Built-in FSM manipulati on functions

Integration

This module integrates with:

cure_types: Core type system operations

cure_parser: Processes parsed AST nodes

cure_smt_solver: Constraint solving for dependent types

cure_type_optimizer: Provides type information for optimizations

Error Categories

Type Mismatches: Incompatible type assignments or operations

Undefined Variables: References to unbound variables

Constraint Violations: Failed dependent type constraints

Export Errors: Missing or incorrectly typed exported functions

Import Errors: Invalid module imports or type mismatches

Performance

Two-Pass Efficiency: Minimizes redundant type checking

Incremental Checking: Supports incremental compilation scenarios

Constraint Caching: Reuses constraint solving results where possible

Environment Sharing: Efficient environment management

Thread Safety

The type checker is stateless and thread-safe. Multiple type checking operations can run concurrently on different ASTs.

Summary

Functions

builtin_env()

check_dependent_constraint(Constraint, Value, Type)

check_expression(Expr, Env)

check_expression(Expr, Env, ExpectedType)

check_fsm/2

check_function/2

check_module/2

check_program(AST)

Type checks an entire Cure program.

convert_and_resolve_record_field_tuple/2

convert_record_field_def/1

convert_type_to_tuple/1

create_function_type_from_signature(Params, ReturnType)

create_function_type_from_signature_records(Params, ReturnType)

extract_and_add_type_params(TypeExpr, Env)

extract_module_functions(AST)

extract_type_param_value/2

extract_type_params_helper/2

get_stdlib_function_type(Module, Name, Arity)

infer_dependent_type(Expr, Env)

infer_type(Expr, Env)

load_stdlib_modules()

Functions

builtin_env()

check_dependent_constraint(Constraint, Value, Type)

check_expression(Expr, Env)

check_expression(Expr, Env, ExpectedType)

check_fsm/2

check_function/2

check_module/2

check_program(AST)

Type checks an entire Cure program.

Performs comprehensive type checking of all top-level items in the program including modules, functions, FSMs, and type definitions.

Arguments

AST - List of top-level AST items from the parser

Returns

typecheck_result() - Complete type checking results including:

success - Boolean indicating overall success/failure

type - Program type (usually undefined for programs)

errors - List of type checking errors found

warnings

List of warnings found

Example

AST = cure_parser:parse_file("example.cure"),
Result = cure_typechecker:check_program(AST),
case Result#typecheck_result.success of
  true ->
    cure_utils:debug("Program type checks successfully~n");

  false ->
    lists:foreach(fun(Error) ->
      cure_utils:debug("Error: ~s~n", [Error#typecheck_error.message])
    end, Result#typecheck_result.errors)
end.

Features

Built-in Environment: Uses standard built-in types and functions

Error Recovery: Continues checking after errors to find more issues

Two-Pass Processing: Collects signatures before checking implementations".

convert_and_resolve_record_field_tuple/2

convert_record_field_def/1

convert_type_to_tuple/1

create_function_type_from_signature(Params, ReturnType)

create_function_type_from_signature_records(Params, ReturnType)

extract_and_add_type_params(TypeExpr, Env)

extract_module_functions(AST)

extract_type_param_value/2

extract_type_params_helper/2

get_stdlib_function_type(Module, Name, Arity)

-spec get_stdlib_function_type(atom(), atom(), integer()) -> {ok, term()} | not_found.

infer_dependent_type(Expr, Env)

infer_type(Expr, Env)

load_stdlib_modules()

cure_types

Cure Programming Language - Type System Core

The core type system module implementing Cure's advanced dependent type system with constraint solving, type inference, and support for higher-kinded types. This module provides the foundational type operations that power Cure's static type checking and dependent type verification.

Key Features

Dependent Types

Value Dependencies: Types that depend on runtime values (e.g., Vector(T, n))

Constraint Solving: SMT-based constraint solving for dependent type verification

Type-Level Computation: Evaluation of type expressions with value parameters

Advanced Type System

Higher-Kinded Types: Support for type constructors and type families

Recursive Types: μ-types with cycle detection and well-formedness checking

Union Types: Discriminated union types with exhaustiveness checking

Generic Types: Full parametric polymorphism with constraint-based inference

Type Inference Engine

Bidirectional Inference: Combines bottom-up and top-down type inference

Constraint Generation: Generates and solves complex type constraints

Alternative Generation: Provides multiple type possibilities with confidence scores

Local Inference: Context-aware type inference for improved accuracy

Unification Algorithm

Robinson Unification: Extended Robinson unification for dependent types

Occurs Check: Prevents infinite types with comprehensive cycle detection

Constraint Propagation: Propagates type constraints through unification

Substitution Management: Efficient substitution composition and application

Core Operations

Type Variables

%% Create new type variables
TVar1 = cure_types:new_type_var(),
TVar2 = cure_types:new_type_var(custom_name).

%% Check type variable properties
true = cure_types:is_type_var(TVar1),
false = cure_types:occurs_check(TVar1, IntType).

Type Unification

%% Unify two types
{ok, Substitution} = cure_types:unify(Type1, Type2),
{ok, Sub, Constraints} = cure_types:unify(Type1, Type2, Environment).

Type Inference

%% Basic type inference
{ok, InferredType} = cure_types:infer_type(Expression, Environment),

%% Enhanced inference with alternatives
{ok, Result} = cure_types:enhanced_infer_type(Expression, Environment),
Confidence = Result#enhanced_inference_result.confidence,
Alternatives = Result#enhanced_inference_result.alternatives.

Type Environment

The type environment maintains variable bindings and constraints:

Hierarchical Scoping: Supports nested scopes with parent environments

Constraint Accumulation: Collects and manages type constraints

Efficient Lookup: Fast variable resolution with scope traversal

%% Environment operations
Env1 = cure_types:new_env(),
Env2 = cure_types:extend_env(Env1, variable_name, VariableType),
{ok, Type} = cure_types:lookup_env(Env2, variable_name).

Constraint Solving

Supports various constraint types:

Equality: T = U

Subtyping: T <: U

Element Membership: x elem_of T

Length Constraints: length(xs) = n

Logical Constraints: implies, iff

Variance Constraints: covariant, contravariant

Higher-Kinded Types

%% Create type constructors
ListKind = cure_types:create_kind('*', [], '*'),
FunctorKind = cure_types:create_kind('->', [ListKind], ListKind),

%% Type families
Family = cure_types:create_type_family(map, [F, T], Dependencies, Constraints),
Result = cure_types:evaluate_type_family(Family, Arguments).

Performance Characteristics

Type Inference: O(n log n) for most expressions

Unification: O(n) for structural types, O(n²) worst case

Constraint Solving: Depends on constraint complexity, uses SMT solver

Memory Usage: Efficient substitution sharing reduces memory overhead

Integration

This module integrates with:

Type Checker: Provides core type operations for checking

SMT Solver: Delegates complex constraint solving

Type Optimizer: Provides types for optimization decisions

Parser: Processes type annotations and expressions

Error Handling

Returns structured errors for:

Unification Failures: Detailed mismatch information

Constraint Violations: Specific constraint failure reasons

Infinite Types: Occurs check violations

Kind Errors: Higher-kinded type mismatches

Thread Safety

Type variables use a global counter that should be accessed safely in concurrent environments. The module is otherwise stateless and thread-safe.

Summary

Functions

apply_type_constructor(TypeConstructor, Args, Location)

bidirectional_infer(Expr, ExpectedType, Env)

check_constraint_satisfaction(Constraint, KindEnv)

check_dependent_constraint(Constraint, Value, Env)

check_higher_kinded_well_formed(HKType)

check_kind(Type, ExpectedKind, KindEnv)

check_recursive_convergence(OldSubst, NewSubst, RecState)

Checks if recursive constraint solving has converged.

check_recursive_type_well_formed/1

check_type(Expr, ExpectedType, Env)

check_type/4

constraint_propagation(Constraints, InitialSubst)

create_kind(Constructor, Args, Location)

create_recursive_type(Name, Params, Definition, Location)

create_type_constructor(Name, Kind, Params, Definition, Location)

create_type_family(Name, Kind, Equations, Location)

detect_cycles/2

enhanced_constraint_solving(Constraints, InitialSubst)

enhanced_infer_type(Expr, Env)

enhanced_infer_type(Expr, Env, Constraints)

evaluate_type_family(TypeFamily, Args)

evaluate_type_predicate/2

extend_env/3

Extends a type environment with a new variable binding.

extract_param_info(Param1, Param2)

extract_type_param_names(TypeParams)

Extract type parameter names from a list that may contain atoms or records.

extract_vector_params/1

fold_recursive_type(Type, Name)

free_type_vars/1

Find all free type variables in a type.

free_type_vars_in_env/1

Find all free type variables in a type environment.

fresh_type_vars_for_params(TypeParams)

Create fresh type variables for a list of type parameters.

generalize_type(Type, Env)

Generalize a type by quantifying over free type variables.

generate_list_alternatives/3

generate_type_alternatives(Expr, InferredType, Env)

get_tuple_param_info/1

infer_dependent_type(Expr, Env)

infer_kind(Type, KindEnv)

infer_pattern_type/3

infer_recursive_function_call(FunctionName, Args, Env, RecState)

Performs type inference for recursive function calls with dependent type tracking.

infer_type(Expr, Env)

infer_type(Expr, Env, Constraints)

infer_with_alternatives(Expr, ExpectedType, Env)

instantiate_poly_type/1

Instantiate a poly_type record with fresh type variables.

instantiate_poly_type/2

Instantiate a poly_type record with provided type arguments.

instantiate_polymorphic_type/2

Instantiate a polymorphic type with fresh type variables.

instantiate_polymorphic_type_if_needed/1

Instantiate a polymorphic type if needed, handling both poly_type and regular types.

instantiate_type_if_function(Type)

is_generic_type_variable_name(Name)

is_nat_type/1

Checks if a type expression represents the Nat type.

is_saturated_type(Type)

is_type_var/1

Checks if a term is a type variable.

is_well_formed_type/1

kind_arity(Kind)

local_type_inference(Expr, InferredType, Env)

lookup_env/2

Looks up a variable binding in the type environment.

nat_from_int/1

Converts an Erlang integer to Peano-encoded Nat.

nat_succ(Nat)

Constructs the successor of a natural number.

nat_to_int/1

Converts a Peano-encoded Nat to an Erlang integer.

nat_zero()

Constructs the Zero value of the Nat type.

new_env()

Creates a new empty type environment.

new_recursive_state()

Creates a new recursive inference state for tracking recursive function calls.

new_type_var()

Creates a new unique type variable without a specific name.

new_type_var(Name)

Creates a new unique type variable with an optional name.

normalize_type(Type)

occurs_check/2

Performs an occurs check to prevent infinite types during unification.

occurs_check_recursive/2

pop_recursive_call(State)

Pops a recursive function call context from the call stack.

push_recursive_call(FunctionName, ParameterTypes, ReturnType, State)

Pushes a recursive function call context onto the call stack.

safe_extract_param_value/1

solve_bounds_constraint(Type, Bounds, Subst)

solve_constraints(Constraints)

solve_constraints/2

solve_equivalence_constraint(Left, Right, Subst)

solve_implication_constraint(Left, Right, Subst)

solve_invariant_constraint(Type, InvariantSpec, Subst)

solve_recursive_constraints_fixed_point(Constraints, RecState)

Solves recursive type constraints using fixed-point computation.

solve_type_family_equation(Equation, Args, KindEnv)

solve_variance_constraint(TypeConstructor, ParameterType, Variance, Subst)

substitute(Type, Subst)

track_dependent_constraints_in_recursion(Constraints, Context, RecState)

Tracks dependent constraints within recursive function calls.

type_to_string/1

unfold_recursive_type/1

unfold_recursive_type/2

unify(Type1, Type2)

Unifies two types using the Robinson unification algorithm.

unify(Type1, Type2, Subst)

Unifies two types with an existing substitution.

unify_kinds(Kind1, Kind2)

unify_recursive_types(RecType1, RecType2, Subst)

unify_with_recursive_context(Types1, Types2, Context, RecState)

Performs unification with recursive context tracking.

Functions

apply_type_constructor(TypeConstructor, Args, Location)

bidirectional_infer(Expr, ExpectedType, Env)

check_constraint_satisfaction(Constraint, KindEnv)

check_dependent_constraint(Constraint, Value, Env)

check_higher_kinded_well_formed(HKType)

check_kind(Type, ExpectedKind, KindEnv)

check_recursive_convergence(OldSubst, NewSubst, RecState)

Checks if recursive constraint solving has converged.

Convergence is determined by comparing the change in substitutions between iterations.

Arguments

OldSubst - Previous substitution

NewSubst - Current substitution

RecState - Recursive inference state with convergence threshold

Returns

{converged, FinalSubst} - If convergence achieved

{not_converged, MergedSubst} - If more iterations needed

check_recursive_type_well_formed/1

check_type(Expr, ExpectedType, Env)

check_type/4

constraint_propagation(Constraints, InitialSubst)

create_kind(Constructor, Args, Location)

create_recursive_type(Name, Params, Definition, Location)

create_type_constructor(Name, Kind, Params, Definition, Location)

create_type_family(Name, Kind, Equations, Location)

detect_cycles/2

enhanced_constraint_solving(Constraints, InitialSubst)

enhanced_infer_type(Expr, Env)

enhanced_infer_type(Expr, Env, Constraints)

evaluate_type_family(TypeFamily, Args)

evaluate_type_predicate/2

extend_env/3

Extends a type environment with a new variable binding.

Supports multiple environment representations for different use cases.

Arguments

Env - Type environment (type_env(), map(), or list())

Var - Variable name (atom())

Type - Type expression to bind to the variable

Returns

Updated environment with the new binding

Supported Environment Types

type_env(): Full environment with constraints and parent scopes

map(): Simple map for lightweight inference

list(): Association list for basic scoping

Example

Env1 = cure_types:new_env(),
Env2 = cure_types:extend_env(Env1, x, {primitive_type, 'Int'}),
Env3 = cure_types:extend_env(Env2, y, {primitive_type, 'String'}).

extract_param_info(Param1, Param2)

extract_type_param_names(TypeParams)

Extract type parameter names from a list that may contain atoms or records.

Arguments

TypeParams - List of atoms or #type_param_decl{} records

Returns

List of type parameter name atoms

extract_vector_params/1

fold_recursive_type(Type, Name)

free_type_vars/1

Find all free type variables in a type.

Arguments

Type - Type expression to analyze

Returns

Set of type variable names/ids that appear free in the type

free_type_vars_in_env/1

Find all free type variables in a type environment.

Arguments

Env - Type environment

Returns

Set of type variable names/ids that appear free in any type in the environment

fresh_type_vars_for_params(TypeParams)

Create fresh type variables for a list of type parameters.

Arguments

TypeParams - List of type parameter atoms or #type_param_decl{} records

Returns

A map from type parameter names to fresh type variables

Example

FreshVars = fresh_type_vars_for_params(['T', 'U']).
% Result: #{'T' => TypeVar1, 'U' => TypeVar2}

generalize_type(Type, Env)

Generalize a type by quantifying over free type variables.

Implements Hindley-Milner let-polymorphism by creating a poly_type that quantifies over type variables that are free in the type but not free in the environment.

Arguments

Type - Type to generalize

Env - Current type environment

Returns

Either a poly_type (if there are free type variables) or the original type

Example

% Type: T -> T where T is free
% Env: {x: Int}
% Result: forall T. T -> T
Type = {function_type, [TypeVar], TypeVar},
Generalized = generalize_type(Type, Env).

generate_list_alternatives/3

generate_type_alternatives(Expr, InferredType, Env)

get_tuple_param_info/1

infer_dependent_type(Expr, Env)

infer_kind(Type, KindEnv)

infer_pattern_type/3

infer_recursive_function_call(FunctionName, Args, Env, RecState)

Performs type inference for recursive function calls with dependent type tracking.

This is the main entry point for recursive function call type inference that properly handles dependent types across recursive boundaries.

Arguments

FunctionName - Name of the recursive function

Args - Argument expressions

Env - Type environment

RecState - Recursive inference state

Returns

{ok, ResultType, Constraints, UpdatedState} - Successful inference

{error, Reason} - Type inference failure

Features

Dependent Type Tracking: Maintains dependent relationships across calls

Fixed-Point Computation: Iterates until type constraints converge

Constraint Propagation: Propagates constraints between recursive levels

Cycle Detection: Prevents infinite recursion in type inference

infer_type(Expr, Env)

infer_type(Expr, Env, Constraints)

infer_with_alternatives(Expr, ExpectedType, Env)

instantiate_poly_type/1

Instantiate a poly_type record with fresh type variables.

Handles the poly_type AST record which explicitly represents polymorphic types with forall quantification.

Arguments

PolyType - A #poly_type{} record

Returns

The instantiated body type with fresh type variables

instantiate_poly_type/2

Instantiate a poly_type record with provided type arguments.

Handles explicit type application where concrete types are provided for type parameters (e.g., id<Int> applies Int to identity function).

Arguments

PolyType - A #poly_type{} record

TypeArgs - List of concrete types to substitute for type parameters

Returns

The instantiated body type with type arguments substituted

instantiate_polymorphic_type/2

Instantiate a polymorphic type with fresh type variables.

Given a type with type parameters (e.g., forall T. T -> T), creates a new type with fresh type variables replacing all type parameters.

Arguments

Type - The polymorphic type to instantiate

TypeParams - List of type parameter names to instantiate (e.g., ['T', 'U'])

Returns

The instantiated type with fresh type variables

Example

PolyType = {function_type, [{primitive_type, 'T'}], {primitive_type, 'T'}},
InstType = instantiate_polymorphic_type(PolyType, ['T']).
% Result: {function_type, [TypeVar1], TypeVar1} where TypeVar1 is fresh

instantiate_polymorphic_type_if_needed/1

Instantiate a polymorphic type if needed, handling both poly_type and regular types.

This is the main entry point for type instantiation during inference. It handles:

poly_type records: Instantiates with fresh type variables

Regular function types: Uses existing instantiate_type_if_function

Other types: Returns as-is

Arguments

Type - Any type expression

Returns

Instantiated type with fresh type variables for polymorphic types

instantiate_type_if_function(Type)

is_generic_type_variable_name(Name)

is_nat_type/1

Checks if a type expression represents the Nat type.

Recognizes both the algebraic Nat type (union type with Zero/Succ) and the refined Nat type (non-negative integers).

Arguments

Type - Type expression to check

Returns

true - If the type is Nat or Nat-related

false - Otherwise

Example

true = cure_types:is_nat_type({primitive_type, 'Nat'}),
true = cure_types:is_nat_type({union_type, 'Nat', _, _}),
true = cure_types:is_nat_type({refined_type, 'Int', ...}).

is_saturated_type(Type)

is_type_var/1

Checks if a term is a type variable.

Arguments

Term - Any term to check

Returns

true - If the term is a type_var record

false - Otherwise

Example

TVar = cure_types:new_type_var(),
true = cure_types:is_type_var(TVar),
false = cure_types:is_type_var(my_atom).

is_well_formed_type/1

kind_arity(Kind)

local_type_inference(Expr, InferredType, Env)

lookup_env/2

Looks up a variable binding in the type environment.

Searches the current environment and parent environments if available.

Arguments

Env - Type environment (type_env(), map(), or list())

Var - Variable name to look up (atom())

Returns

Type - The type bound to the variable if found

undefined - If the variable is not bound in the environment

Scoping

For type_env() records, searches parent environments if the variable is not found in the current scope.

Example

Env = cure_types:extend_env(cure_types:new_env(), x, IntType),
IntType = cure_types:lookup_env(Env, x),
undefined = cure_types:lookup_env(Env, unbound_var).

nat_from_int/1

Converts an Erlang integer to Peano-encoded Nat.

Creates a chain of Succ constructors wrapping Zero, representing the given non-negative integer.

Arguments

N - Non-negative integer

Returns

{ok, NatExpr} - Peano-encoded natural number

{error, negative_integer} - If N < 0

Example

{ok, Three} = cure_types:nat_from_int(3),
%% Results in Succ(Succ(Succ(Zero)))

nat_succ(Nat)

Constructs the successor of a natural number.

In Peano encoding, Succ(n) represents n+1, similar to Idris's S constructor.

Arguments

Nat - A natural number expression

Returns

An expression representing Succ(Nat) : Nat

Example

One = cure_types:nat_succ(cure_types:nat_zero()),
Two = cure_types:nat_succ(One),
%% Results in Succ(Succ(Zero))

nat_to_int/1

Converts a Peano-encoded Nat to an Erlang integer.

Unwraps the chain of Succ constructors to compute the integer value.

Arguments

NatExpr - Peano-encoded natural number expression

Returns

{ok, Integer} - The integer value

{error, invalid_nat} - If not a valid Nat expression

Example

{ok, Three} = cure_types:nat_from_int(3),
{ok, 3} = cure_types:nat_to_int(Three).

nat_zero()

Constructs the Zero value of the Nat type.

In Peano encoding, Zero is the base case for natural numbers, similar to Idris's Z constructor.

Returns

An expression representing Zero : Nat

Example

Zero = cure_types:nat_zero(),
%% Results in an identifier expression representing Zero

new_env()

Creates a new empty type environment.

The type environment maintains variable bindings, constraints, and supports hierarchical scoping through parent environments.

Returns

type_env() - A new empty type environment

Example

Env = cure_types:new_env(),
Env2 = cure_types:extend_env(Env, x, {primitive_type, 'Int'}),
{ok, Type} = cure_types:lookup_env(Env2, x).

Features

Hierarchical Scoping: Supports nested environments

Constraint Tracking: Accumulates type constraints

Efficient Lookup: Fast variable resolution

new_recursive_state()

Creates a new recursive inference state for tracking recursive function calls.

Returns

recursive_inference_state() - New state with empty call stack

Example

State = cure_types:new_recursive_state(),
UpdatedState = cure_types:push_recursive_call(factorial, ParamTypes, RetType, State).

new_type_var()

Creates a new unique type variable without a specific name.

This is a convenience function that calls new_type_var/1 with undefined name.

Returns

type_var() - A new unique type variable

Example

TVar = cure_types:new_type_var(),
true = cure_types:is_type_var(TVar).

Note

Uses a process dictionary counter to ensure uniqueness within a process. For concurrent use, external synchronization may be required.

new_type_var(Name)

Creates a new unique type variable with an optional name.

Arguments

Name - Optional name for the type variable (atom() | undefined)

Returns

type_var() - A new unique type variable with the given name

Example

TVar1 = cure_types:new_type_var(my_var),
TVar2 = cure_types:new_type_var(undefined),
true = TVar1#type_var.name =:= my_var.

Note

The name is primarily for debugging and error reporting. The unique ID ensures type variable identity regardless of name.

normalize_type(Type)

occurs_check/2

Performs an occurs check to prevent infinite types during unification.

The occurs check ensures that a type variable does not occur within the type it would be unified with, preventing infinite type structures.

Arguments

TypeVar - Type variable to check for

Type - Type expression to check within

Returns

true - If the type variable occurs in the type (would create infinite type)

false - If the unification would be safe

Example

TVar = cure_types:new_type_var(),
ListType = {list_type, TVar},
true = cure_types:occurs_check(TVar, ListType),  % Would create infinite list
false = cure_types:occurs_check(TVar, {primitive_type, 'Int'}).

Note

This is essential for preventing infinite types like T = List(T) during unification.

occurs_check_recursive/2

pop_recursive_call(State)

Pops a recursive function call context from the call stack.

Arguments

State - Current recursive inference state

Returns

{ok, Context, NewState} - Popped context and updated state

{error, empty_stack} - If the call stack is empty

push_recursive_call(FunctionName, ParameterTypes, ReturnType, State)

Pushes a recursive function call context onto the call stack.

This tracks recursive calls to enable proper dependent type handling across recursive boundaries.

Arguments

FunctionName - Name of the function being called recursively

ParameterTypes - Types of the parameters in this call

ReturnType - Expected return type of the function

State - Current recursive inference state

Returns

{ok, NewState} - Updated state with the call pushed

{error, Reason} - If maximum recursion depth exceeded

Example

{ok, NewState} = cure_types:push_recursive_call(
    factorial, [NType], FactorialRetType, State
).

safe_extract_param_value/1

solve_bounds_constraint(Type, Bounds, Subst)

solve_constraints(Constraints)

solve_constraints/2

solve_equivalence_constraint(Left, Right, Subst)

solve_implication_constraint(Left, Right, Subst)

solve_invariant_constraint(Type, InvariantSpec, Subst)

solve_recursive_constraints_fixed_point(Constraints, RecState)

Solves recursive type constraints using fixed-point computation.

This function iteratively refines type constraints until they converge, handling dependent types that may change across recursive calls.

Arguments

Constraints - List of type constraints to solve

RecState - Recursive inference state

Returns

{ok, Substitution, Iterations} - Converged solution

{error, Reason} - If convergence fails or max iterations exceeded

Algorithm

Apply current substitution to constraints

Solve constraints to get new substitution

Check for convergence by comparing substitutions

Repeat until convergence or max iterations reached

solve_type_family_equation(Equation, Args, KindEnv)

solve_variance_constraint(TypeConstructor, ParameterType, Variance, Subst)

substitute(Type, Subst)

track_dependent_constraints_in_recursion(Constraints, Context, RecState)

Tracks dependent constraints within recursive function calls.

This function maintains the relationships between dependent types across recursive call boundaries, ensuring type safety.

Arguments

Constraints - Type constraints from the current call

Context - Recursive call context

RecState - Current recursive inference state

Returns

{ok, TrackedConstraints, UpdatedState} - Success with tracked constraints

{error, Reason} - If constraint tracking fails

type_to_string/1

unfold_recursive_type/1

unfold_recursive_type/2

unify(Type1, Type2)

Unifies two types using the Robinson unification algorithm.

This is a convenience function that calls unify/3 with an empty substitution.

Arguments

Type1 - First type expression to unify

Type2 - Second type expression to unify

Returns

{ok, Substitution} - Successful unification with substitution map

{error, Reason} - Unification failure with detailed error

Example

{ok, Subst} = cure_types:unify(IntType, IntType),
{ok, Subst2} = cure_types:unify(TVar, IntType),
{error, _} = cure_types:unify(IntType, StringType).

Error Cases

Type mismatch (e.g., Int vs String)

Occurs check failure (infinite types)

Constraint violations

unify(Type1, Type2, Subst)

Unifies two types with an existing substitution.

Applies the existing substitution to both types before unification and composes the results.

Arguments

Type1 - First type expression to unify

Type2 - Second type expression to unify

Subst - Existing substitution map to compose with

Returns

{ok, NewSubstitution} - Combined substitution after unification

{error, Reason} - Unification failure with detailed error

Example

{ok, Subst1} = cure_types:unify(TVar1, IntType),
{ok, Subst2} = cure_types:unify(TVar2, StringType, Subst1),
%% Subst2 now contains bindings for both TVar1 and TVar2

Substitution Composition

The function applies the input substitution to both types before unification and composes the result with the input substitution.

unify_kinds(Kind1, Kind2)

unify_recursive_types(RecType1, RecType2, Subst)

unify_with_recursive_context(Types1, Types2, Context, RecState)

Performs unification with recursive context tracking.

This extends the standard unification algorithm to properly handle type variables and dependent types across recursive call boundaries.

Arguments

Types1 - First set of types to unify

Types2 - Second set of types to unify

Context - Recursive call context

RecState - Recursive inference state

Returns

{ok, Constraints, UpdatedState} - Successful unification with constraints

{error, Reason} - Unification failure

cure_utils

Summary

Functions

debug(Format)

debug(Format, Data)

Functions

debug(Format)

-spec debug(Format) -> ok when Format :: io:format().

debug(Format, Data)

-spec debug(Format, Data) -> ok when Format :: io:format(), Data :: [term()].