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.

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.

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.

Dependent Type Parser Support

This module provides parser helper functions for dependent type syntax introduced in Phase 6. It extends the main parser with support for

Dependent Type Checking with SMT

This module implements type checking for dependent types, extending the base type checker with support for

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.

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.

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

Cure FSM Runtime Verification

This module implements runtime verification for FSMs by generating monitors from verified properties and injecting runtime assertions.

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.

FSM Type Safety

This module provides enhanced type checking for FSM definitions, ensuring

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.

Guard-Based Type Refinement

This module implements Phase 3 of the guard support implementation: type system integration for guard constraints.

Enhanced SMT Guard Verification

Phase 4 enhancement for guard analysis using Z3 SMT solver.

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.

LSP Code Actions & Quick Fixes

This module provides automated fixes and suggestions for constraint violations

LSP Rich Diagnostics with SMT Counterexamples

This module enhances LSP diagnostics with

LSP Performance Optimization

This module provides performance optimizations for real-time LSP verification

Cure Language Server Protocol (LSP) Implementation

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

Type Holes - Interactive Type Inference

Provides Idris-style type holes where you can write

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.

Optimizations specifically for pipe operator chains.

Cure Runtime Profiler

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

Refinement Types with SMT Verification

This module implements refinement types - types augmented with logical predicates that are verified at compile-time using the Z3 SMT solver.

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.

Native Erlang implementations of Show trait functions for Cure.

SMT Array Theory for Lists and Vectors

This module provides SMT array theory support for reasoning about lists and vectors with constraints like

Cure SMT Model Parser

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

Cure SMT Solver Process Manager

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

SMT Solver Integration for Cure

This module provides integration with SMT (Satisfiability Modulo Theories) solvers for dependent type constraint verification and optimization. It supports multiple backend solvers including Z3, CVC5, and others.

Cure SMT-LIB Translator

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

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.

Native Erlang implementations of string operations for Cure.

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.

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.

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.