# Route Specs and Forms

Iwf uses Idris types to keep routes, links, request decoding, and forms in
agreement. The public interface should still feel like ordinary web code:
route strings, input records, handlers, `pathTo`, and literal HTML forms.

The internal dependent representation exists so the compiler can prove things
for you. Application code should not destructure route internals by hand.

## The User-Facing Rule

Write a handlerless route spec from the HTTP method, path, and declared input
types, then bind the handler:

```idris
record ArticleForm where
  constructor MkArticleForm
  title : String
  description : String
  body : String
  tagList : Maybe String

createArticle : ArticleForm -> ControllerContext -> Response
createArticle input context =
  ...

createArticleRoute : RouteSpec NoInput ArticleForm Response
createArticleRoute =
  post "/editor" |> body ArticleForm |> html

createArticleBinding : BoundRoute
createArticleBinding =
  handledBy createArticleRoute createArticle
```

The body type belongs to the route spec. `handledBy` reads the type of
`createArticle` at compile time, sees `ArticleForm -> ControllerContext ->
Response`, and checks that the handler implements the spec.

Do not write an adapter that pulls fields out of the decoded body. The binding
macro generates that adapter.

## Path and Query Records

Route strings name path and query inputs:

```idris
record ArticleInput where
  constructor MkArticleInput
  slug : String

articleShow : ArticleInput -> ControllerContext -> Response
articleShow input context =
  render context (articlePage input.slug)

articleRoute : RouteSpec ArticleInput NoInput Response
articleRoute =
  get "/articles/{slug}" |> params ArticleInput |> html

articleBinding : BoundRoute
articleBinding =
  handledBy articleRoute articleShow
```

The `{slug}` capture belongs to `ArticleInput.slug`. A request for
`/articles/hello-world` calls:

```idris
articleShow (MkArticleInput "hello-world") context
```

Query fields work the same way:

```idris
record ArticleListInput where
  constructor MkArticleListInput
  tag : Maybe String
  limit : Maybe Integer
  offset : Maybe Integer

articleList : ArticleListInput -> ControllerContext -> Response
articleList input context =
  render context (articleListPage input)

articleListRoute : RouteSpec ArticleListInput NoInput Response
articleListRoute =
  get "/articles?{tag}&{limit}&{offset}" |> params ArticleListInput |> html

articleListBinding : BoundRoute
articleListBinding =
  handledBy articleListRoute articleList
```

Optional query inputs are `Maybe` fields. Repeated query inputs are `List`
fields.

## Path or Query Plus Body

When a route has both URL inputs and a request body, use two records:

```idris
record CommentInput where
  constructor MkCommentInput
  slug : String

record CommentBody where
  constructor MkCommentBody
  body : String

createComment : CommentInput -> CommentBody -> ControllerContext -> Response
createComment input body context =
  createCommentForArticle input.slug body.body context

commentRoute : RouteSpec CommentInput CommentBody Response
commentRoute =
  post "/articles/{slug}/comments" |> params CommentInput |> body CommentBody |> html

commentBinding : BoundRoute
commentBinding =
  handledBy commentRoute createComment
```

The first record is matched against the route string. Fields named in the path
or query pattern come from the URL. The second record is the request body.

That rule also applies to JSON routes:

```idris
createCommentApi : CommentInput -> CommentBody -> ControllerContext -> CommentEnvelope
createCommentApi input body context =
  MkCommentEnvelope input.slug body.body

createCommentApiRoute : RouteSpec CommentInput CommentBody CommentEnvelope
createCommentApiRoute =
  post "/api/articles/{slug}/comments"
    |> params CommentInput
    |> body CommentBody
    |> respondsJson CommentEnvelope

createCommentApiBinding : BoundRoute
createCommentApiBinding =
  handledBy createCommentApiRoute createCommentApi
```

When a route spec declares a JSON response type, `handledBy` checks that the
handler returns that type and wraps it as JSON.

## What Gets Checked

From this declaration:

```idris
post "/articles/{slug}/comments?{notify}"
  |> params CommentInput
  |> body CommentBody
  |> html
```

and this handler type:

```idris
createComment : CommentInput -> CommentBody -> ControllerContext -> Response
```

Iwf checks:

- `slug` comes from the path.
- `notify`, if present on the first record, comes from the query string.
- fields on `CommentBody` come from the declared request body.
- the request body can be decoded before user code runs.
- OpenAPI request metadata can be derived when schema information is available.

If the route string and first handler record do not agree, compilation fails.
For example, a route with `{slug}` needs a compatible `slug` field.

## Links

Use `pathTo` instead of string concatenation:

```idris
articlePath : String
articlePath =
  pathTo articleRoute (MkArticleInput "hello-world")
```

Routes without path or query inputs need no input record:

```idris
homePath : String
homePath =
  pathTo homeRoute
```

The route value decides the call shape. If it has required path inputs, `pathTo`
expects a record. If it has no path or query inputs, `pathTo` returns a
`String` directly.

## Forms

Forms stay literal HTML:

```idris
commentForm : Article -> CommentBody -> Html
commentForm article input =
  <form method="post" action={pathTo commentRoute (MkCommentInput article.slug)}>
    <textarea name={commentBodyBodyField}>{input.body}</textarea>
    <button type="submit">Post comment</button>
  </form>
```

`commentBodyBodyField` is generated from `CommentBody.body` by `FormFields`.
When IDRX sees that field inside a form whose action is `pathTo commentRoute`,
it checks that the route body accepts a `body : String` field.

That catches common mistakes:

- a form field name no longer exists on the body record.
- a form field has the right name but the wrong Idris type.
- a form points at a route whose body record does not contain that field.

The source code remains normal HTML. The proof work happens in generated Idris
terms.

## Request Decoding

The same body record is used for browser forms and JSON requests. The server
chooses the decoder from `Content-Type`:

- `application/json` decodes JSON fields.
- `application/x-www-form-urlencoded` decodes browser form fields.
- `multipart/form-data` decodes text fields and typed upload fields when the
  route supports file uploads.

This keeps HTML forms, JSON clients, validation, and OpenAPI metadata aligned
around one handler type.

## Route Specs and Runtime Bindings

Iwf has two route layers:

- `RouteSpec params body response`, the importable route contract used by
  views, redirects, forms, and OpenAPI docs.
- `BoundRoute`, the executable route produced by `handledBy` and used in
  `Routes`.

Normal applications write named `RouteSpec` declarations by starting with the
HTTP method and path, then piping in URL params, request body, and response
metadata. They then assemble `BoundRoute` bindings in a runtime route list:

```idris
export
htmlHomeRoute : RouteSpec NoInput NoInput Response
htmlHomeRoute =
  get "/" |> html

export
htmlHomeBinding : BoundRoute
htmlHomeBinding =
  handledBy htmlHomeRoute home

export
htmlArticleRoute : RouteSpec ArticleInput NoInput Response
htmlArticleRoute =
  get "/articles/{slug}" |> params ArticleInput |> html

export
htmlArticleBinding : BoundRoute
htmlArticleBinding =
  handledBy htmlArticleRoute articleShow

export
htmlCommentRoute : RouteSpec CommentInput CommentBody Response
htmlCommentRoute =
  post "/articles/{slug}/comments" |> params CommentInput |> body CommentBody |> html

export
htmlCommentBinding : BoundRoute
htmlCommentBinding =
  handledBy htmlCommentRoute createComment

export
htmlRoutes : Routes
htmlRoutes =
  [ htmlHomeBinding
  , htmlArticleBinding
  , htmlCommentBinding
  ]
```

The route macros build importable specs. `handledBy` builds the runtime route
entry and generates the typed decoding adapter from the spec and handler type.

## What Bugs This Prevents

These mistakes fail before the server starts:

- a route path mentions a field missing from the handler input record.
- a query field has an unsupported or mismatched Idris type.
- a link omits required route input.
- a form submits a field that is not in the request body record.
- a form field has a stale generated name after a record rename.
- a JSON or form request body no longer matches the handler type.

The point is not that users write dependent types. The point is that users
write normal records and HTML while the compiler checks the wiring.