Skip to content

Commit b6446cd

Browse files
Claude/ephapax linear types e00 zs (#6)
* 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) --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 8a60f91 commit b6446cd

29 files changed

Lines changed: 1650 additions & 0 deletions

library/common/arithmetic/add.md

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+
```
Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
# Operation: contains
2+
3+
## Interface Signature
4+
5+
```
6+
contains: Collection[A], A -> Boolean
7+
```
8+
9+
## Behavioral Semantics
10+
11+
**Purpose**: Determines whether a collection contains a specific element.
12+
13+
**Parameters**:
14+
- `collection`: The source collection of elements of type `A`
15+
- `element`: The element to search for
16+
17+
**Return Value**: `true` if `element` is found in `collection`, otherwise `false`.
18+
19+
**Properties**:
20+
- Empty collection: `contains([], x) = false` for all `x`
21+
- Single element match: `contains([x], x) = true`
22+
- Single element no match: `contains([x], y) = false` when `x ≠ y`
23+
- Can be expressed as: `contains(c, x) = greater_than(length(filter(c, e => equal(e, x))), 0)`
24+
25+
**Edge Cases**:
26+
- Equality comparison semantics (reference vs value) is implementation-defined
27+
- Short-circuit evaluation (stop on first match) is implementation-defined
28+
- Search order and performance characteristics are implementation-defined
29+
30+
## Executable Test Cases
31+
32+
```yaml
33+
test_cases:
34+
- input:
35+
collection: [1, 2, 3, 4, 5]
36+
element: 3
37+
output: true
38+
description: "Element is present in collection"
39+
40+
- input:
41+
collection: [1, 2, 3, 4, 5]
42+
element: 6
43+
output: false
44+
description: "Element is not present in collection"
45+
46+
- input:
47+
collection: []
48+
element: 1
49+
output: false
50+
description: "Empty collection contains no elements"
51+
52+
- input:
53+
collection: [1]
54+
element: 1
55+
output: true
56+
description: "Single element collection contains that element"
57+
58+
- input:
59+
collection: ["a", "b", "c"]
60+
element: "b"
61+
output: true
62+
description: "String element is present"
63+
64+
- input:
65+
collection: [1, 2, 1, 3, 1]
66+
element: 1
67+
output: true
68+
description: "Element appears multiple times (still returns true)"
69+
```

0 commit comments

Comments
 (0)