Skip to content

Commit 8821598

Browse files
committed
docs: regenerate documentation for v4.1.0 release
Update README structure and all formal documentation with production links, Code Standards section, and improved formatting.
1 parent c29a21c commit 8821598

9 files changed

Lines changed: 2140 additions & 2252 deletions

README.md

Lines changed: 83 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,54 @@
11
# Functional Programming Library for Ada 2022
22

3-
[![License](https://img.shields.io/badge/license-BSD--3--Clause-blue.svg)](LICENSE) [![Ada](https://img.shields.io/badge/Ada-2022-blue.svg)](https://ada-lang.io) [![SPARK](https://img.shields.io/badge/SPARK-Proved-brightgreen.svg)](https://www.adacore.com/about-spark) [![Alire](https://img.shields.io/badge/Alire-2.0+-blue.svg)](https://alire.ada.dev)
3+
[![License](https://img.shields.io/badge/license-BSD--3--Clause-blue.svg)](LICENSE) [![Ada](https://img.shields.io/badge/Ada-2022-blue.svg)](https://ada-lang.io) [![SPARK](https://img.shields.io/badge/SPARK-Proved-green.svg)](https://www.adacore.com/about-spark) [![Alire](https://img.shields.io/badge/Alire-2.0+-blue.svg)](https://alire.ada.dev)
44

5-
**Version:** 4.0.0
6-
**Date:** December 12, 2025
5+
**Version:** 4.1.0<br>
6+
**Date:** 2025-12-18<br>
77
**SPDX-License-Identifier:** BSD-3-Clause<br>
88
**License File:** See the LICENSE file in the project root<br>
9-
**Copyright:** © 2025 Michael Gardner, A Bit of Help, Inc.<br>
10-
**Status:** Released
9+
**Copyright:** © 2025 Michael Gardner, A Bit of Help, Inc.<br>
10+
**Status:** Released
1111

1212
## Overview
1313

1414
A production-ready Ada 2022 library providing functional programming abstractions for type-safe computation. Implements `Result<T,E>`, `Option<T>`, `Either<L,R>` monadic types, and `Scoped` RAII guards with 80+ composable operations enabling railway-oriented programming, explicit error handling, optional value management, and automatic resource cleanup.
1515

1616
Designed for safety-critical, embedded, and high-assurance applications with full SPARK compatibility.
1717

18+
## Features
19+
20+
### Core Types (80+ operations)
21+
22+
| Type | Operations | Purpose |
23+
|------|------------|---------|
24+
| **Result[T,E]** | 30 | Success/failure with typed errors |
25+
| **Option[T]** | 25 | Optional values (presence/absence) |
26+
| **Either[L,R]** | 20 | Disjoint unions (one of two types) |
27+
| **Try** | 6 + child packages | Exception-to-functional bridges |
28+
| **Scoped** | 2 | RAII resource guards |
29+
30+
### Embedded Systems Ready
31+
32+
- **Preelaborate/Pure** categorization on all packages
33+
- **Zero heap allocation** - Stack-based discriminated records only
34+
- **No controlled types in core** - No finalization overhead
35+
- **No tasking dependencies** - Ravenscar profile compatible
36+
- **Bounded memory** - Fixed-size structures
37+
- **No OS dependencies** - Pure Ada 2022
38+
39+
### Production Quality
40+
41+
- **Comprehensive test coverage** (90%+ code coverage)
42+
- **Zero dependencies** - Ada 2022 standard library only
43+
- **Comprehensive contracts** - Pre/Post conditions throughout
44+
- **Cross-platform** - POSIX and Windows tested
45+
1846
## SPARK Formal Verification
1947

2048
<table>
2149
<tr>
2250
<td width="120"><strong>Status</strong></td>
23-
<td><img src="https://img.shields.io/badge/SPARK-Proved-brightgreen.svg" alt="SPARK Proved"></td>
51+
<td><img src="https://img.shields.io/badge/SPARK-Proved-green.svg" alt="SPARK Proved"></td>
2452
</tr>
2553
<tr>
2654
<td><strong>Scope</strong></td>
@@ -50,11 +78,11 @@ make spark-check # Run SPARK legality verification
5078
make spark-prove # Run full SPARK proof verification
5179
```
5280

53-
### Verified Packages
81+
### SPARK Coverage
5482

5583
| Package | SPARK_Mode | Description |
5684
|---------|-----------|-------------|
57-
| `Functional.Result` | On | Result[T,E] monad (33 operations) |
85+
| `Functional.Result` | On | Result[T,E] monad (30 operations) |
5886
| `Functional.Option` | On | Option[T] monad (25 operations) |
5987
| `Functional.Either` | On | Either[L,R] type (20 operations) |
6088
| `Functional.Version` | On | Version information |
@@ -71,41 +99,6 @@ Since SPARK only analyzes instantiated generics (not generic templates), the lib
7199
- **Helper function verification**: All predicates and transformers formally proven overflow-safe
72100
- **High proof rate**: See [CHANGELOG](CHANGELOG.md) for current statistics
73101

74-
## Features
75-
76-
### Core Types (85+ operations)
77-
78-
| Type | Operations | Purpose |
79-
|------|------------|---------|
80-
| **Result[T,E]** | 33 | Success/failure with typed errors |
81-
| **Option[T]** | 25 | Optional values (presence/absence) |
82-
| **Either[L,R]** | 20 | Disjoint unions (one of two types) |
83-
| **Try** | 7 | Exception-to-functional bridges |
84-
| **Scoped** | 2 | RAII resource guards |
85-
86-
### SPARK Formal Verification
87-
88-
- **SPARK_Mode => On** for Option, Result, Either, Version (formally verifiable)
89-
- **SPARK_Mode => Off** for Try only (exception boundary, by design)
90-
- **Postconditions** on all transform operations for prover assistance
91-
- **Preconditions** on all extractors preventing invalid access
92-
93-
### Embedded Systems Ready
94-
95-
- **Preelaborate/Pure** categorization on all packages
96-
- **Zero heap allocation** - Stack-based discriminated records only
97-
- **No controlled types** - No finalization overhead
98-
- **No tasking dependencies** - Ravenscar profile compatible
99-
- **Bounded memory** - Fixed-size structures
100-
- **No OS dependencies** - Pure Ada 2022
101-
102-
### Production Quality
103-
104-
- **Comprehensive test coverage** (90%+ code coverage)
105-
- **Zero dependencies** - Ada 2022 standard library only
106-
- **Comprehensive contracts** - Pre/Post conditions throughout
107-
- **Cross-platform** - POSIX and Windows tested
108-
109102
## Quick Start
110103

111104
### Installation
@@ -114,7 +107,7 @@ Add to your `alire.toml`:
114107

115108
```toml
116109
[[depends-on]]
117-
functional = "^3.0.0"
110+
functional = "^4.1.0"
118111
```
119112

120113
Then build:
@@ -202,26 +195,42 @@ Result := Str_Int.Fold (E, On_String'Access, On_Integer'Access);
202195

203196
### Try - Exception Boundaries
204197

198+
Use `Map_To_Result_With_Param` (recommended) for declarative exception mapping:
199+
205200
```ada
206-
with Functional.Try;
201+
with Functional.Try.Map_To_Result_With_Param;
202+
203+
package Try_Read is new Functional.Try.Map_To_Result_With_Param
204+
(Error_Kind_Type => Error_Kind,
205+
Param_Type => String,
206+
Result_Type => IO_Result.Result,
207+
Make_Error => Make_Error,
208+
Default_Error_Kind => Internal_Error,
209+
Action => Read_File_Raw);
207210
208-
-- Bridge exception-based code to Result
209-
function Safe_Parse is new Functional.Try.Try_To_Functional_Result
210-
(T => Integer, E => Error, Result_Pkg => Int_Result,
211-
Map_Exception => To_Error, Action => Integer'Value);
211+
Mappings : constant Try_Read.Mapping_Array :=
212+
[(Name_Error'Identity, Not_Found),
213+
(Use_Error'Identity, Permission_Error)];
212214
213-
R := Safe_Parse; -- Never raises, returns Result
215+
Result := Try_Read.Run (File_Path, Mappings);
216+
```
217+
218+
Use `Try_To_Option_With_Param` for probe operations:
219+
220+
```ada
221+
-- Returns None on any exception, then use Unwrap_Or
222+
Exists := Bool_Option.Unwrap_Or (Try_Is_TZif (Path), False);
214223
```
215224

216225
## API Reference
217226

218-
### Result<T,E> (33 operations)
227+
### Result<T,E> (30 operations)
219228

220229
| Category | Operations |
221230
|----------|------------|
222231
| **Constructors** | `Ok`, `New_Error`, `From_Error` |
223232
| **Predicates** | `Is_Ok`, `Is_Error`, `Is_Ok_And`, `Is_Error_And`, `Is_Ok_Or`, `Is_Error_Or`, `Contains` |
224-
| **Extractors** | `Value`, `Error_Info` |
233+
| **Extractors** | `Value`, `Error` |
225234
| **Defaults** | `Unwrap_Or`, `Unwrap_Or_With` |
226235
| **Transforms** | `Map`, `Map_Or`, `Map_Or_Else`, `And_Then`, `And_Then_Into`, `Map_Error`, `Bimap`, `Zip_With`, `Flatten`, `To_Option` |
227236
| **Recovery** | `Fallback`, `Fallback_With`, `Recover`, `Recover_With` |
@@ -255,17 +264,16 @@ R := Safe_Parse; -- Never raises, returns Result
255264
| **Conversion** | `To_Option`, `To_Result` |
256265
| **Operators** | `"="` (Contains) |
257266

258-
### Try Module (7 functions)
267+
### Try Module (6 functions + child packages)
259268

260269
| Function | Purpose |
261270
|----------|---------|
262-
| `Try_To_Result` | General bridge for any Result type |
263-
| `Try_To_Functional_Result` | Convenience for Functional.Result |
264271
| `Try_To_Functional_Option` | Convenience for Functional.Option |
265-
| `Try_To_Result_With_Param` | Parameterized Result bridge |
266272
| `Try_To_Option_With_Param` | Parameterized Option bridge |
267273
| `Map_To_Result` | Declarative exception mapping tables |
268274
| `Map_To_Result_With_Param` | Parameterized declarative mapping |
275+
| `Try_To_Result` | General bridge (deprecated) |
276+
| `Try_To_Functional_Result` | Convenience for Functional.Result (deprecated) |
269277

270278
### Scoped Module (2 generic packages)
271279

@@ -287,24 +295,18 @@ make test-unit
287295
make test-coverage
288296
```
289297

290-
**Results:** 269 tests passing (Result: 84, Option: 65, Either: 58, Try: 14, Try_Option: 6, Scoped: 11, Map_To_Result: 31)
298+
**Results:** All tests passing. See [CHANGELOG](CHANGELOG.md) for current counts.
291299

292300
## Documentation
293301

294-
- **[Cheatsheet](docs/guides/cheatsheet.md)** - All 87 operations at a glance
302+
- **[Cheatsheet](docs/guides/cheatsheet.md)** - All operations at a glance
295303
- **[User Guide](docs/guides/user_guide.md)** - Design philosophy, SPARK, embedded, best practices
296304
- **[Quick Start](docs/quick_start.md)** - Get started in minutes
297305
- **[SRS](docs/formal/software_requirements_specification.md)** - Requirements specification
298306
- **[SDS](docs/formal/software_design_specification.md)** - Design specification
299307
- **[STG](docs/formal/software_test_guide.md)** - Test guide
300308
- **[CHANGELOG](CHANGELOG.md)** - Release history
301309

302-
## Code Standards
303-
304-
This project follows:
305-
- **Ada Agent** (`~/.claude/agents/ada.md`)
306-
- **Functional Agent** (`~/.claude/agents/functional.md`)
307-
308310
## Submodule Management
309311

310312
```bash
@@ -313,6 +315,12 @@ make submodule-update # Pull latest
313315
make submodule-status # Check commits
314316
```
315317

318+
## Code Standards
319+
320+
This project follows:
321+
- **Ada Agent** (`~/.claude/agents/ada.md`) - Ada 2022 standards
322+
- **Functional Agent** (`~/.claude/agents/functional.md`) - Result/Option/Either patterns
323+
316324
## Contributing
317325

318326
This project is not open to external contributions at this time.
@@ -344,14 +352,14 @@ A Bit of Help, Inc.
344352

345353
## Project Status
346354

347-
**Status**: Production Ready (v4.0.0)
348-
349-
- Result[T,E] - 33 operations
350-
- Option[T] - 25 operations
351-
- Either[L,R] - 20 operations
352-
- Try module - 7 exception bridges
353-
- Scoped module - 2 RAII guard packages
354-
- SPARK compatible (Option, Result, Either, Version)
355-
- Comprehensive test coverage (90%+)
356-
- Zero external dependencies
357-
- Cross-platform (POSIX, Windows)
355+
**Status**: Production Ready (v4.1.0)
356+
357+
- [x] Result[T,E] - 30 operations
358+
- [x] Option[T] - 25 operations
359+
- [x] Either[L,R] - 20 operations
360+
- [x] Try module - 6 functions + child packages
361+
- [x] Scoped module - 2 RAII guard packages
362+
- [x] SPARK compatible (see CHANGELOG for proof stats)
363+
- [x] Comprehensive test coverage (see CHANGELOG)
364+
- [x] Zero external dependencies
365+
- [x] Cross-platform (POSIX, Windows)

docs/diagrams/.gitkeep

Whitespace-only changes.

0 commit comments

Comments
 (0)