TEA-specialised routing integration for ReScript, built on top of cadre-router.
┌─────────────────────────────────────────────────────────────┐
│ cadre-tea-router │
│ • Route → Msg patterns │
│ • URL subscriptions │
│ • Navigation Cmds (push/replace/back/forward) │
│ • init-from-URL helpers │
└─────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────┐
│ cadre-router │
│ • URL parsing/formatting combinators │
│ • Route definitions │
│ • Framework-agnostic primitives │
└─────────────────────────────────────────────────────────────┘This repository provides TEA/Elm-Architecture wiring:
-
Route → Msg patterns
-
init-from-URL helpers
-
Subscriptions for URL changes
-
Cmd helpers for navigation (push/replace/back/forward)
-
TEA-focused examples
-
Re-implementing URL parsing/formatting combinators (belongs to
cadre-router). -
Framework-agnostic routing primitives (belongs to
cadre-router). -
React-specific routing APIs unless they are explicitly TEA-driven.
npm install @anthropics/cadre-tea-router @anthropics/cadre-routerAdd to rescript.json:
{
"bs-dependencies": [
"@anthropics/cadre-router",
"@anthropics/cadre-tea-router"
]
}// Define your routes using cadre-router
module Routes = {
open CadreRouter
let home = root
let users = s("users")
let user = s("users") / int
}
// Wire into TEA with cadre-tea-router
module App = {
open CadreTeaRouter
type route =
| Home
| Users
| User(int)
| NotFound
type msg =
| UrlChanged(route)
| Navigate(route)
| ...
let parseRoute = url => {
open Routes
switch url {
| url if home->matches(url) => Home
| url if users->matches(url) => Users
| url => user->parse(url)->Option.mapOr(NotFound, id => User(id))
}
}
let subscriptions = _ => {
Router.urlChanges(url => UrlChanged(parseRoute(url)))
}
let update = (msg, model) => {
switch msg {
| Navigate(route) => (model, Router.push(routeToUrl(route)))
| UrlChanged(route) => ({...model, route}, Cmd.none)
| ...
}
}
}cadre-tea-router integrates with proven for unbreakable URL parsing. The ProvenSafeUrl module provides mathematical guarantees that URL operations cannot crash:
open ProvenSafeUrl
// Formally verified URL parsing
let parseRoute = (urlString: string) => {
switch parse(urlString) {
| Ok(url) => {
// url.pathname is guaranteed to be well-formed
// No undefined behavior, no crashes
switch url.pathname {
| "/users" => Users
| "/posts" => Posts
| _ => NotFound
}
}
| Error(_) => NotFound // Invalid URLs mathematically excluded
}
}
// Safe query parameter extraction
let getUserId = (url: string) => {
switch getQueryParam(url, "id") {
| Ok(Some(id)) => Some(id)
| Ok(None) | Error(_) => None
}
}Traditional URL parsers rely on runtime validation and can fail in unexpected ways:
-
Buffer overruns on malformed URLs
-
Undefined behavior on edge cases
-
Silent failures that corrupt application state
Proven’s SafeUrl uses Idris2 dependent types to prove correctness:
-
✓ URLs are either well-formed or return an error (no crashes)
-
✓ Query parameters are safely extracted (no undefined access)
-
✓ Path operations maintain URL validity (no corruption)
These proofs are checked at compile-time in Idris2, ensuring runtime safety in ReScript/JavaScript routing.
cadre-tea-router (Route → Msg patterns)
↓
ProvenSafeUrl (Formally verified URL parsing)
↓
JavaScript Bindings (proven/bindings/javascript)
↓
Zig FFI (proven/ffi/zig)
↓
Idris2 ABI (proven/src/Proven/SafeUrl.idr)
↓
Formally Verified Implementation ✓For more information, see the proven library documentation.
-
cadre-router - Core routing primitives
-
rescript-tea - TEA implementation for ReScript
-
proven - Formally verified library (Idris2)