Skip to content

Commit a287684

Browse files
Claude/ephapax linear types e00 zs (#7)
* feat: Initial Ephapax language implementation Ephapax is a linear type system for safe memory management targeting WebAssembly. This commit includes: Core Implementation: - ephapax-syntax: AST definitions with linear type annotations - ephapax-typing: Linear type checker with region support - ephapax-wasm: WASM code generator with bump allocation - ephapax-runtime: no_std WASM runtime with region management Formal Semantics (Coq): - Syntax.v: Core type and expression definitions - Typing.v: Linear typing rules with context tracking - Semantics.v: Operational semantics and safety theorems Documentation: - Language specification (spec/SPEC.md) - Comprehensive wiki documentation - ROADMAP.md with detailed development plan - CONTRIBUTING.adoc guide Infrastructure: - Cargo workspace with 4 crates - CI/CD workflow for Rust and Coq - EUPL-1.2 license Key features: - Linear types prevent use-after-free and memory leaks - Region-based memory management for bulk deallocation - Second-class borrows for temporary access - Formal proofs in Coq for type safety * feat(frontend): Add lexer and parser for Ephapax language Implements Phase 2 (Language Frontend) of the Ephapax roadmap: - ephapax-lexer: High-performance lexer using logos - Tokenizes all Ephapax syntax (keywords, operators, literals) - Support for nested block comments {- -} - String escape sequence handling - Comprehensive error recovery - 20+ unit tests - ephapax-parser: Parser combinator implementation using chumsky - Complete expression parsing (let, fn, if, region, case, etc.) - Type parsing (base types, String@region, functions, products, sums) - Declaration parsing (fn, type) - Rich error reporting with ariadne - 19 unit tests + doc tests All tests pass successfully. * feat(backend): Add interpreter, REPL, CLI, and standard library - Complete ephapax-typing with full expression type checking (pair, sum types, case, let, string operations) - Add ephapax-interp tree-walking interpreter for debugging - Create ephapax-repl with interactive REPL and commands (:help, :type, :load, :tokens, :reset, :verbose) - Build ephapax-cli with subcommands (run, check, compile, repl) - Add ephapax-stdlib with prelude, I/O, string, math modules - Add compile_module function to ephapax-wasm * chore: Add library folder structure for common and specific libraries Set up directory structure for Ephapax libraries: - library/common/ for shared language implementations - library/specific/ for Ephapax-specific code * feat(library): Add common and specific library specifications Common Library (from aggregate-library): - arithmetic: add, subtract, multiply, divide, modulo - comparison: less_than, greater_than, equal, not_equal, etc. - logical: and, or, not - string: concat, length, substring - collection: map, filter, fold, contains - conditional: if_then_else Ephapax-Specific Library: - linear: move, drop, copy (linear type operations) - region: new_region, alloc_in (region-based memory) - memory: borrow (reference operations) - wasm: compile_to_wasm (WebAssembly compilation) * refactor(library): Reorganize as aggregate-library with common + ephapax Renamed library/ to aggregate-library/ with clearer structure: Common Library (22 ops from hyperpolymath/aggregate-library): - arithmetic: add, subtract, multiply, divide, modulo - comparison: equal, not_equal, less_than, greater_than, less_equal, greater_equal - logical: and, or, not - string: concat, length, substring - collection: map, filter, fold, contains - conditional: if_then_else Ephapax-Specific Library (17 ops): - linear: move, drop, copy, borrow - region: new_region, alloc_in - io: print, println, read_line - conversion: i32_to_string, string_to_i32 - product: pair, fst, snd - sum: inl, inr, case Total: 39 fully-specified operations --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent b6446cd commit a287684

40 files changed

Lines changed: 2039 additions & 0 deletions

aggregate-library/README.md

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
# Ephapax Aggregate Library
2+
3+
The complete standard library for Ephapax = Common Library + Ephapax-Specific Library.
4+
5+
## Structure
6+
7+
```
8+
aggregate-library/
9+
├── common/ # Common Library (22 operations)
10+
│ ├── arithmetic/ # add, subtract, multiply, divide, modulo
11+
│ ├── comparison/ # equal, not_equal, less_than, greater_than, less_equal, greater_equal
12+
│ ├── logical/ # and, or, not
13+
│ ├── string/ # concat, length, substring
14+
│ ├── collection/ # map, filter, fold, contains
15+
│ └── conditional/ # if_then_else
16+
17+
└── ephapax/ # Ephapax-Specific Library (17 operations)
18+
├── linear/ # move, drop, copy, borrow
19+
├── region/ # new_region, alloc_in
20+
├── io/ # print, println, read_line
21+
├── conversion/ # i32_to_string, string_to_i32
22+
├── product/ # pair, fst, snd
23+
└── sum/ # inl, inr, case
24+
```
25+
26+
## Common Library
27+
28+
Universal operations shared across all languages in the aggregate-library ecosystem. These 22 operations represent the intersection of functionality across radically different programming paradigms.
29+
30+
Source: https://github.com/hyperpolymath/aggregate-library
31+
32+
## Ephapax-Specific Library
33+
34+
Operations unique to Ephapax's linear type system and region-based memory management:
35+
36+
### Linear Types (4 operations)
37+
- `move` - Transfer ownership of linear values
38+
- `drop` - Explicitly consume linear values
39+
- `copy` - Duplicate unrestricted values
40+
- `borrow` - Create temporary references
41+
42+
### Regions (2 operations)
43+
- `new_region` - Create scoped memory regions
44+
- `alloc_in` - Allocate in specific regions
45+
46+
### I/O (3 operations)
47+
- `print` - Output string without newline
48+
- `println` - Output string with newline
49+
- `read_line` - Read line from stdin
50+
51+
### Conversion (2 operations)
52+
- `i32_to_string` - Integer to string
53+
- `string_to_i32` - Parse string as integer
54+
55+
### Product Types (3 operations)
56+
- `pair` - Construct pairs
57+
- `fst` - Extract first element
58+
- `snd` - Extract second element
59+
60+
### Sum Types (3 operations)
61+
- `inl` - Inject left
62+
- `inr` - Inject right
63+
- `case` - Pattern match on sum
64+
65+
## Total: 39 Operations
66+
67+
Combined, the Ephapax standard library provides 39 fully-specified operations.
Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
# Operation: add
2+
3+
## Interface Signature
4+
5+
```
6+
add: Number, Number -> Number
7+
```
8+
9+
## Behavioral Semantics
10+
11+
**Purpose**: Computes the sum of two numbers.
12+
13+
**Parameters**:
14+
- `a`: The first number (augend)
15+
- `b`: The second number (addend)
16+
17+
**Return Value**: The arithmetic sum of `a` and `b`.
18+
19+
**Properties**:
20+
- Commutative: `add(a, b) = add(b, a)`
21+
- Associative: `add(add(a, b), c) = add(a, add(b, c))`
22+
- Identity element: `add(a, 0) = a`
23+
24+
**Edge Cases**:
25+
- Overflow/underflow behavior is implementation-defined (Standard Library concern)
26+
- NaN and infinity handling is implementation-defined (Standard Library concern)
27+
28+
## Executable Test Cases
29+
30+
```yaml
31+
test_cases:
32+
- input: [2, 3]
33+
output: 5
34+
description: "Basic addition of positive integers"
35+
36+
- input: [-5, 3]
37+
output: -2
38+
description: "Addition with negative number"
39+
40+
- input: [0, 0]
41+
output: 0
42+
description: "Addition of zeros"
43+
44+
- input: [1.5, 2.5]
45+
output: 4.0
46+
description: "Addition of decimal numbers"
47+
48+
- input: [-10, -20]
49+
output: -30
50+
description: "Addition of two negative numbers"
51+
```
Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
# Operation: divide
2+
3+
## Interface Signature
4+
5+
```
6+
divide: Number, Number -> Number
7+
```
8+
9+
## Behavioral Semantics
10+
11+
**Purpose**: Computes the quotient of two numbers.
12+
13+
**Parameters**:
14+
- `a`: The dividend (number to be divided)
15+
- `b`: The divisor (number by which to divide)
16+
17+
**Return Value**: The arithmetic quotient `a ÷ b`.
18+
19+
**Properties**:
20+
- Non-commutative: `divide(a, b) ≠ divide(b, a)` (in general)
21+
- Identity element: `divide(a, 1) = a`
22+
- Inverse of multiplication: `divide(multiply(a, b), b) = a` (when `b ≠ 0`)
23+
24+
**Preconditions**:
25+
- `b ≠ 0` (division by zero behavior is implementation-defined)
26+
27+
**Edge Cases**:
28+
- Division by zero is implementation-defined (Standard Library concern)
29+
- May return error, infinity, or NaN depending on language
30+
- Integer vs floating-point division is implementation-defined
31+
- Overflow/underflow behavior is implementation-defined
32+
- NaN and infinity handling is implementation-defined
33+
34+
## Executable Test Cases
35+
36+
```yaml
37+
test_cases:
38+
- input: [6, 2]
39+
output: 3
40+
description: "Basic division with exact result"
41+
42+
- input: [7, 2]
43+
output: 3.5
44+
description: "Division with fractional result"
45+
46+
- input: [0, 5]
47+
output: 0
48+
description: "Zero divided by non-zero"
49+
50+
- input: [-10, 2]
51+
output: -5
52+
description: "Division with negative dividend"
53+
54+
- input: [10, -2]
55+
output: -5
56+
description: "Division with negative divisor"
57+
58+
- input: [-12, -3]
59+
output: 4
60+
description: "Division of two negative numbers"
61+
```
Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
# Operation: modulo
2+
3+
## Interface Signature
4+
5+
```
6+
modulo: Number, Number -> Number
7+
```
8+
9+
## Behavioral Semantics
10+
11+
**Purpose**: Computes the remainder of division of two numbers.
12+
13+
**Parameters**:
14+
- `a`: The dividend (number to be divided)
15+
- `b`: The divisor (number by which to divide)
16+
17+
**Return Value**: The remainder when `a` is divided by `b`.
18+
19+
**Properties**:
20+
- Non-commutative: `modulo(a, b) ≠ modulo(b, a)` (in general)
21+
- `modulo(a, b)` has the same sign as the divisor in most implementations
22+
- For positive integers: `0 ≤ modulo(a, b) < b` when `b > 0`
23+
24+
**Preconditions**:
25+
- `b ≠ 0` (modulo by zero behavior is implementation-defined)
26+
27+
**Edge Cases**:
28+
- Modulo by zero is implementation-defined (Standard Library concern)
29+
- Sign of result with negative operands is implementation-defined
30+
- Some languages use truncated division (result has sign of dividend)
31+
- Others use floored division (result has sign of divisor)
32+
- Behavior with floating-point numbers is implementation-defined
33+
34+
## Executable Test Cases
35+
36+
```yaml
37+
test_cases:
38+
- input: [7, 3]
39+
output: 1
40+
description: "Basic modulo with positive integers"
41+
42+
- input: [10, 5]
43+
output: 0
44+
description: "Modulo with no remainder"
45+
46+
- input: [15, 4]
47+
output: 3
48+
description: "Modulo returning non-zero remainder"
49+
50+
- input: [0, 5]
51+
output: 0
52+
description: "Zero modulo non-zero"
53+
54+
- input: [100, 7]
55+
output: 2
56+
description: "Modulo with larger numbers"
57+
```
58+
59+
**Note**: Test cases with negative numbers are omitted due to implementation-defined behavior across languages.
Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
# Operation: multiply
2+
3+
## Interface Signature
4+
5+
```
6+
multiply: Number, Number -> Number
7+
```
8+
9+
## Behavioral Semantics
10+
11+
**Purpose**: Computes the product of two numbers.
12+
13+
**Parameters**:
14+
- `a`: The multiplicand (first factor)
15+
- `b`: The multiplier (second factor)
16+
17+
**Return Value**: The arithmetic product `a × b`.
18+
19+
**Properties**:
20+
- Commutative: `multiply(a, b) = multiply(b, a)`
21+
- Associative: `multiply(multiply(a, b), c) = multiply(a, multiply(b, c))`
22+
- Identity element: `multiply(a, 1) = a`
23+
- Zero property: `multiply(a, 0) = 0`
24+
- Distributive over addition: `multiply(a, add(b, c)) = add(multiply(a, b), multiply(a, c))`
25+
26+
**Edge Cases**:
27+
- Overflow/underflow behavior is implementation-defined (Standard Library concern)
28+
- NaN and infinity handling is implementation-defined (Standard Library concern)
29+
30+
## Executable Test Cases
31+
32+
```yaml
33+
test_cases:
34+
- input: [2, 3]
35+
output: 6
36+
description: "Basic multiplication of positive integers"
37+
38+
- input: [-5, 3]
39+
output: -15
40+
description: "Multiplication with negative number"
41+
42+
- input: [0, 42]
43+
output: 0
44+
description: "Multiplication by zero"
45+
46+
- input: [7, 1]
47+
output: 7
48+
description: "Multiplication by one (identity)"
49+
50+
- input: [2.5, 4]
51+
output: 10.0
52+
description: "Multiplication with decimal number"
53+
54+
- input: [-3, -4]
55+
output: 12
56+
description: "Multiplication of two negative numbers"
57+
```
Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Operation: subtract
2+
3+
## Interface Signature
4+
5+
```
6+
subtract: Number, Number -> Number
7+
```
8+
9+
## Behavioral Semantics
10+
11+
**Purpose**: Computes the difference between two numbers.
12+
13+
**Parameters**:
14+
- `a`: The minuend (number from which another is subtracted)
15+
- `b`: The subtrahend (number to be subtracted)
16+
17+
**Return Value**: The arithmetic difference `a - b`.
18+
19+
**Properties**:
20+
- Non-commutative: `subtract(a, b) ≠ subtract(b, a)` (in general)
21+
- Identity element: `subtract(a, 0) = a`
22+
- Inverse of addition: `subtract(add(a, b), b) = a`
23+
24+
**Edge Cases**:
25+
- Overflow/underflow behavior is implementation-defined (Standard Library concern)
26+
- NaN and infinity handling is implementation-defined (Standard Library concern)
27+
28+
## Executable Test Cases
29+
30+
```yaml
31+
test_cases:
32+
- input: [5, 3]
33+
output: 2
34+
description: "Basic subtraction of positive integers"
35+
36+
- input: [3, 5]
37+
output: -2
38+
description: "Subtraction resulting in negative number"
39+
40+
- input: [0, 0]
41+
output: 0
42+
description: "Subtraction of zeros"
43+
44+
- input: [-5, 3]
45+
output: -8
46+
description: "Subtracting positive from negative"
47+
48+
- input: [10.5, 2.5]
49+
output: 8.0
50+
description: "Subtraction of decimal numbers"
51+
52+
- input: [-10, -20]
53+
output: 10
54+
description: "Subtracting negative from negative"
55+
```

0 commit comments

Comments
 (0)