Skip to content
Logo

Routing and gates

Pages are data

structure ReflApp (β : Type) where
  init     : Doc
  pages    : List (String × RView)     -- path → view
  handlers : List RHandler
  gates    : List (String × String) := []
  binding  : Option β := none

pages maps a path to the view rendered at that path. The current path is the path scalar, so navigation is an ordinary state change:

⟨"nav", [ .setInput "path" ]⟩

and a navigating control is any control that fires it:

.btn "My posts →" "padding:8px" "nav" (.str "/my_posts")

ViewDsl.navTo and ViewDsl.goTo wrap that pattern.

Because the page table is data, tooling can check it. nav-integrity.mjs walks every page view and fails if any static navigation target is not a registered page — no reachable-but-unrouted link can survive the gate.

Gates — guards that run before the lookup

gates : List (String × String) := []   -- (scalar, page)

A gate says: whenever this scalar is empty, render this page, whatever the path says. They are evaluated in order, before the path lookup.

gates := [ ("connected", "/connect"), ("onboarded", "/profile") ]

Read: an unconnected user always lands on /connect; a connected but un-onboarded user always lands on /profile; everyone else gets the page their path names.

Why this is a framework feature and not app code

Without gates, every page is reachable by setting path. Nothing forces a user through onboarding — which is exactly how a profile pre-filled with a fixture name went unnoticed in a real app. The failure is silent: every screen renders, every test passes, and the app simply never enforces its own entry sequence.

The alternative — wrapping each page in a .cond — was tried and rejected. It duplicated the guard screens into all 23 pages and tripled the bundle. A gate costs one check per render.

Gates are declarations, not code

The shape deliberately mirrors what a configuration-driven client declares:

"gates": [ { "when": "!$identity", "page": "/connect" },
           { "when": "!$onboarded", "page": "/profile" } ]

Same statement, now typed and inside the proof boundary — a workflow that navigates to a gated page while the gate scalar is empty will prove it lands on the guard page.

Browser history

The web runtime wires pushState and popstate so the browser Back button works and deep links resolve. A workflow can assert that behaviour with the back step:

steps := [ .fire "nav" (.atom (.str "/my_posts")), .back ]

WStep.back is identity in the proof — browser history is a runtime concern, not part of the Doc model — and is genuinely executed by the replayers (goBack). Assert its effect with a ui check rather than a Doc check, since the proof tier cannot see it.

Coverage

page-coverage.mjs enforces a bijection:

  • every registered page is reached by some workflow, and
  • every path a workflow reaches is a registered page.

Both directions bite. The first catches a screen nobody tests; the second catches a workflow navigating to a path that does not exist — a typo that would otherwise render blank. When this gate was added it immediately found an uncovered page in the flagship app and an uncovered entry route in hello.

Recap

  • Pages map paths to views; the current path is the path scalar, making navigation an ordinary state change.
  • Gates are (scalar, page) pairs evaluated in order before the path lookup, enforcing entry sequences.
  • A gate says: when this scalar is empty, render this page regardless of what path says.
  • Gates are declarations, not code, so workflows can prove they land on the correct guard page.
  • The web runtime wires pushState and popstate for browser history and deep linking.
  • page-coverage.mjs ensures every page is reached by a workflow and every navigated path exists.

Next steps

  • Views — defining the page views that routing dispatches to
  • Effects — the setInput effect that drives scalar state changes
  • Workflows — testing navigation with fire and back steps