System Architecture

System Architecture

This page provides a detailed overview of the Pie interpreter's architecture, explaining the key components and their interactions.

High-Level Overview

The Pie interpreter follows a three-level architecture that separates syntax, elaborated expressions, and runtime values:

┌─────────────┐      ┌─────────────┐      ┌─────────────┐
│    Source   │─────▶│    Core     │─────▶│    Value    │
│ (User Code) │      │(Elaborated) │      │ (Runtime)   │
└─────────────┘      └─────────────┘      └─────────────┘
                                                 │
                                                 ▼
                                          ┌─────────────┐
                                          │    Core     │
                                          │ (Normalized)│
                                          └─────────────┘

The system processes Pie code through several stages:

1. Parsing: Convert text to Source AST
2. Type Checking: Transform Source to Core while checking types
3. Evaluation: Execute Core to produce Values
4. Normalization: Convert Values back to Core for comparison

Key Components

Parser System

The parser converts input strings to abstract syntax trees (ASTs) in two stages:

1. Scheme Parser: Converts the input into a Scheme-like S-expression
2. Pie Parser: Converts the S-expression into a Pie-specific AST

Key files:

• src/pie_interpreter/parser/parser.ts

Parser Flow

Input String → Scheme Lexer → Scheme Parser → Pie Parser → Source AST

Main Components

Source

Source represents the original syntax as written by the programmer:

• Contains location information for error reporting
• Defines type checking methods (check, synth, isType)
• Describes the syntactic structure before elaboration

Key files:

• src/pie_interpreter/types/source.ts

Core

Core represents the elaborated, fully type-checked expressions:

• Focused on evaluation and normalization
• Serves as the intermediary between source syntax and runtime values

Key files:

• src/pie_interpreter/types/core.ts

Value

Value represents the semantic meaning of expressions during evaluation:

• Captures runtime values during type checking and execution
• Has methods for normalization (converting back to Core)
• Includes lazy evaluation support through the now() method

Key files:

• src/pie_interpreter/types/value.ts
• src/pie_interpreter/types/neutral.ts

Type Checker

The type checker verifies that Pie programs are well-typed, following bidirectional type checking with three primary operations:

Type Checking Flow

┌────────────┐
│ Expression │
└─────┬──────┘
      │
   ┌──▼──┐ No   ┌───────────┐
   │Synth├──────▶ Check     │
   └──┬──┘      │ Against T │
      │ Yes     └─────┬─────┘
      │               │
┌─────▼───────┐  ┌────▼─────┐
│  Type T +   │  │Elaborated│
│Elaborated E │  │    E     │
└─────────────┘  └──────────┘

• isType: Verifies that an expression is a valid type
• synth: Synthesizes the type of an expression without a type annotation
• check: Verifies that an expression has a given type

Key files:

• src/pie_interpreter/typechecker/represent.ts
• src/pie_interpreter/typechecker/synthesizer.ts
• src/pie_interpreter/typechecker/utils.ts

Evaluator

The evaluator implements the operational semantics of Pie expressions through a call-by-need evaluation strategy:

Evaluation Process

┌──────┐    ┌──────┐    ┌──────┐
│ Core │───▶│Value │───▶│ Core │
└──────┘    └──────┘    └──────┘
  valOf       now/     readBack
             readBack

• Value Evaluation: Each Core expression has a valOf method that evaluates it to a Value
• Specialized Evaluators: Functions like doApp, doIndNat, etc. handle different expression types
• Normalization by Evaluation: The readBack functions convert Values back to Core expressions
• Call-by-need Evaluation: Uses lazy evaluation through the Delay type and now() method

Key files:

• src/pie_interpreter/evaluator/evaluator.ts
• src/pie_interpreter/evaluator/utils.ts

Error Handling

The error handling system uses a monadic approach with Perhaps<T>:

Error Handling Flow

┌────────────┐   success   ┌────────────┐
│ Operation1 ├─────────────▶ Operation2 │
└─────┬──────┘             └─────┬──────┘
      │ failure                  │ failure
      ▼                          ▼
┌────────────┐            ┌────────────┐
│  Error     │            │  Error     │
│  Message   │            │  Message   │
└────────────┘            └────────────┘

• Perhaps Type: Represents computations that might succeed or fail
  • go<T>: Contains a successful result of type T
  • stop: Contains an error message and location
• PerhapsM Type: A mutable container for passing results from computations
• goOn Function: Sequences computations that may fail

Key files:

• src/pie_interpreter/types/utils.ts

Tactics System

The tactics system enables structured proof development:

Tactics System Architecture

┌───────────┐    ┌───────────┐    ┌───────────┐
│ ProofState│◄───┤   Tactic  │◄───┤    User   │
└─────┬─────┘    └───────────┘    └───────────┘
      │
      │
┌─────▼─────┐
│ ProofState│
│  Updated  │
└─────┬─────┘
      │
      ▼
┌───────────┐
│  Final    │
│  Proof    │
└───────────┘

• ProofState: Tracks current goals and proof environment
• Tactics: Operate on the ProofState to transform goals
• ProofManager: Manages the application of tactics to proofs

Key files:

• src/pie_interpreter/tactics/proofstate.ts
• src/pie_interpreter/tactics/tactics.ts
• src/pie_interpreter/tactics/proofmanager.ts

Directory Structure

src/pie_interpreter/
├── parser/                # Parsing functionality
│   └── parser.ts
├── types/                 # Core type definitions
│   ├── source.ts          # Source AST
│   ├── core.ts            # Core expressions
│   ├── value.ts           # Runtime values
│   ├── neutral.ts         # Neutral expressions
│   └── utils.ts           # Utilities and monads
├── typechecker/           # Type checking
│   ├── represent.ts
│   ├── synthesizer.ts
│   └── utils.ts
├── evaluator/             # Evaluation and normalization
│   ├── evaluator.ts
│   └── utils.ts
├── tactics/               # Tactical theorem proving
│   ├── proofstate.ts
│   ├── tactics.ts
│   └── proofmanager.ts
├── utils/                 # Utility functions
│   ├── environment.ts
│   ├── locations.ts
│   ├── context.ts
│   ├── fresh.ts
│   └── alphaeqv.ts
└── __tests__/             # Test files