# Forms and Validation

Iwf forms are normal HTML forms backed by typed routes and input records. The
route decides where the form submits. The input record decides which fields are
accepted.

## 1. Define The Input Record

Create a record for the submitted fields:

```idris
record SettingsForm where
  constructor MkSettingsForm
  email : String
  username : String
  bio : Maybe String
```

Derive form fields:

```idris
%runElab derive "SettingsForm" [Show, Eq, FormFields]
```

This generates field values such as:

```idris
settingsFormEmailField : FormField SettingsForm "email" String
settingsFormUsernameField : FormField SettingsForm "username" String
```

When you rename a record field, the generated field value changes too. Stale
form field names fail at compile time.

## 2. Define The Submit Route

A handler with a body record receives decoded form data:

```idris
saveSettings : SettingsForm -> ControllerContext -> Response
saveSettings input context =
  case validateSettings input of
    Left errors => renderValidation context input errors settingsPage
    Right valid =>
      flashInContext "notice" "Settings saved" context
        (seeOther (pathTo settingsRoute))

settingsRoute : RouteSpec NoInput SettingsForm Response
settingsRoute =
  put "/settings" |> body SettingsForm |> html

settingsBinding : BoundRoute
settingsBinding =
  handledBy settingsRoute saveSettings
```

For routes with path/query params and body fields, use two records:

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

The first record comes from the URL. The second record comes from the request
body.

## 3. Render The Form

In `.idrx`, write normal HTML:

```idris
settingsForm : SettingsForm -> List ValidationError -> Html
settingsForm input errors =
  <form id="settings-form" class="form stack" method="post" action={pathTo settingsRoute}>
    {errorSummary errors}
    <label class="field">
      <span>Email</span>
      <input name={settingsFormEmailField} value={input.email} type="email" />
    </label>
    <label class="field">
      <span>Username</span>
      <input name={settingsFormUsernameField} value={input.username} />
    </label>
    <button class="btn-primary" type="submit">Update settings</button>
  </form>
```

`render` injects the CSRF hidden input into non-GET forms.

Route-backed forms are HTMX-enhanced by default when the `.idrx` macro can see
the target route. Write the form action directly as `action={pathTo ...}` and
Iwf renders the matching HTMX verb attribute:

```html
<form action="/settings" hx-patch="/settings" method="POST">
  ...
</form>
```

If the action is a precomputed `String`, the macro cannot recover the route
method or body membership from that string. Keep `pathTo` visible in the form
attribute when you want compile-time field checks and generated HTMX verbs.

Iwf still keeps the native HTML fallback. Browsers without JavaScript only
submit `GET` or `POST`. For a `PUT`, `PATCH`, or `DELETE` route, Iwf accepts
the common method-override pattern:

```html
<form method="post" action="/settings">
  <input type="hidden" name="_method" value="PATCH">
  ...
</form>
```

The browser still sends `POST`, but Iwf reads `_method` and treats the request
as `PATCH` before route matching. Direct forms should spell that hidden field
explicitly when they need a no-JavaScript fallback for `PUT`, `PATCH`, or
`DELETE` routes.

If you write an HTMX-only control yourself, use the HTMX verb directly:

```html
<button hx-patch="/settings" hx-target="#settings-form">Save</button>
```

Use `hx-put`, `hx-patch`, or `hx-delete` for the HTMX request. Keep `_method`
only when the same form should also work as normal HTML without JavaScript.

## 4. Decode And Validate

For simple records:

```idris
settingsFormDecoder : FromFormBody SettingsForm
settingsFormDecoder =
  derivedFromFormBody settingsFormParams settingsFormFromParams
```

Useful validation helpers:

- `requiredString`
- `minLength`
- `matches`
- `fieldError`

Validation returns:

```idris
Either (List ValidationError) value
```

Render errors back to the same page:

```idris
renderValidation context input errors settingsPage
```

Use `renderValidationWithFlashes` when the failed response should also set flash
messages. Submitted values stay in the input record, field errors are rendered,
CSRF still works, and boosted HTMX requests stay on the fragment path.

## 5. Direct Forms Are Canonical

The public surface is literal HTML plus typed values:

- `action={pathTo route ...}` for the route-backed URL.
- Generated `FormField` values for `name` attributes.
- A normal `method`, `enctype`, and optional `_method` hidden field when the
  form needs a browser fallback for non-POST routes.

This keeps the interface inspectable as HTML while still letting Idris check
that field names match the route body at compile time.

## 6. Multipart Forms

Use multipart when the body contains files:

```html
<form method="post" enctype="multipart/form-data" action="/avatar">
  <input type="file" name="avatar" />
  <button type="submit">Upload</button>
</form>
```

Route bodies can contain:

- `UploadedFile`
- `Maybe UploadedFile`
- `List UploadedFile`

Use `multipartFile` for one file and `multipartFilesFor` for repeated uploads
when you need to inspect raw multipart data.

```idris
uploadAvatar : MultipartFormData -> IO (Either String StoredFile)
uploadAvatar formData =
  case multipartFile "avatar" formData of
    Nothing => pure (Left "missing avatar upload")
    Just file =>
      storeUploadedFile
        (localFileStorage (MkLocalFileStorage "uploads" "/uploads"))
        file
```

## 7. CSRF

`render` injects CSRF fields into non-GET forms. Validate submitted forms with:

- `validateSessionCsrf`
- `handleProtectedFormWith`

The CSRF token is stored in the signed session.

For the dependent-type mechanics behind `FormField`, route body membership, and
IDRX form checks, see [Dependent Routes and Forms](dependent-routes-and-forms.md).

## Next

Read [Database and Migrations](database-and-migrations.md).