# First CRUD Feature

This guide builds one small article feature in the order users usually need it:
page, route, form, table, query, validation, auth, live refresh, and final
check. It uses the app-facing `Iwf` surface only.

## 1. Create The App

Start from a generated project:

```sh
iwf new my-app
cd my-app
iwf build
```

Keep the starter shape:

```idris
module Main

import Iwf

%language ElabReflection
%default partial
```

The normal app path starts from `import Iwf`. Add feature imports only when the
feature needs generated app code, such as `Generated.Schema` for database rows.

## 2. Add A Page

Write the page directly. The view returns ordinary `.idrx` HTML; `render`
adds the default shell for full browser requests:

```idris
articleIndexView : Html
articleIndexView =
  fragment
    [ <title>Articles</title>
    , <main id="main-content" class="mx-auto flex max-w-3xl flex-col gap-6 p-6">
        <header class="flex items-center justify-between">
          <h1>Articles</h1>
          <a class="btn-primary" href="/articles/new">New article</a>
        </header>
        <p>No articles yet.</p>
      </main>
    ]
```

`render` serves the full shell for normal browser requests and the
`#main-content` fragment for boosted requests.

## 3. Add A Route With A Path Parameter

Path captures live in a normal record:

```idris
record ArticlePath where
  constructor MkArticlePath
  slug : String
```

The route spec tells Iwf which path fields to decode, and `handledBy` checks
the handler implements that spec:

```idris
showArticle : ArticlePath -> ControllerContext -> ControllerApp Response
showArticle input context = do
  maybeArticle <-
    sqlQuery
      "select articles.* from articles where slug = ${input.slug}"
  article <- requireFound maybeArticle
  pure (render context (articleShowView article))

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

showArticleBinding : BoundRoute
showArticleBinding =
  handledBy showArticleRoute showArticle
```

There is no separate body declaration for this route because the route has no
body. For routes that do have a body, declare the body type on the route spec
and bind the handler with `handledBy`.

## 4. Add A Form

Define the submitted fields:

```idris
record ArticleForm where
  constructor MkArticleForm
  title : String
  slug : String
  body : String

%runElab derive "ArticleForm" [Show, Eq, FormFields]
```

Write the form as direct HTML:

```idris
newArticleForm : ArticleForm -> List ValidationError -> Html
newArticleForm input errors =
  <form id="article-form" class="form stack" method="post" action={pathTo createArticleRoute}>
    {errorSummary errors}
    <label class="field">
      <span>Title</span>
      <input name={articleFormTitleField} value={input.title} />
    </label>
    <label class="field">
      <span>Slug</span>
      <input name={articleFormSlugField} value={input.slug} />
    </label>
    <label class="field">
      <span>Body</span>
      <textarea name={articleFormBodyField}>{input.body}</textarea>
    </label>
    <button class="btn-primary" type="submit">Publish</button>
  </form>
```

The route value supplies the action URL. The generated field values supply the
`name` attributes. If a field is renamed on `ArticleForm`, stale form markup
fails at compile time.

Put the form in a page and route to it:

```idris
newArticlePage : ArticleForm -> List ValidationError -> Html
newArticlePage input errors =
  fragment
    [ <title>New Article</title>
    , <main id="main-content" class="mx-auto flex max-w-3xl flex-col gap-6 p-6">
        <h1>New article</h1>
        {newArticleForm input errors}
      </main>
    ]

newArticle : ControllerContext -> Response
newArticle context =
  render context (newArticlePage (MkArticleForm "" "" "") [])

newArticleRoute : RouteSpec NoInput NoInput Response
newArticleRoute =
  get "/articles/new"

newArticleBinding : BoundRoute
newArticleBinding =
  handledBy newArticleRoute newArticle
```

## 5. Add A Table

Add the table to `Application/Schema.sql`:

```sql
CREATE TABLE articles (
  id BIGSERIAL PRIMARY KEY,
  slug TEXT NOT NULL UNIQUE,
  title TEXT NOT NULL,
  body TEXT NOT NULL,
  created_at TIMESTAMP NOT NULL DEFAULT now()
);
```

Then rebuild:

```sh
iwf build
```

The build generates `Generated.Schema`, including `Article` and typed table
ids. Import it where handlers or views use generated models:

```idris
import Generated.Schema
```

## 6. Add TypedSQL Queries

Write the SQL directly beside the handler code. `sqlQuery` is for statements
that return rows; `sqlExec` is for statements that do not return rows.

Replace the empty page with a data-driven page:

```idris
articleIndexView : ControllerContext -> List Article -> Html
articleIndexView context articles =
  fragment
    [ <title>Articles</title>
    , <main id="main-content" class="mx-auto flex max-w-3xl flex-col gap-6 p-6">
        <header class="flex items-center justify-between">
          <h1>Articles</h1>
          <a class="btn-primary" href="/articles/new">New article</a>
        </header>
        {articleList articles}
      </main>
    ]
```

Run queries directly from the controller. The handler's `ControllerContext`
provides the current database automatically:

```idris
articles : ControllerContext -> ControllerApp Response
articles context = do
  rows <-
    sqlQuery
      "select articles.* from articles order by created_at desc"
  pure (render context (articleIndexView context rows))
```

For writes, use `sqlExec`:

```idris
insertArticle : ArticleForm -> ControllerContext -> ControllerApp ()
insertArticle input context =
  sqlExec
    "insert into articles (slug, title, body) values (${input.slug}, ${input.title}, ${input.body})"
```

## 7. Add Validation

Validate the decoded body record before writing:

```idris
validateArticle : ArticleForm -> Either (List ValidationError) ArticleForm
validateArticle input =
  allValidations
    [ mapValidation (\_ => input) (requiredString "title" input.title)
    , mapValidation (\_ => input) (requiredString "slug" input.slug)
    , mapValidation (\_ => input) (requiredString "body" input.body)
    ]
    (valid input)
```

Use the same page when validation fails:

```idris
createArticle : ArticleForm -> ControllerContext -> ControllerApp Response
createArticle input context =
  case validateSessionCsrf context.session context.request of
    Left errors => pure (render context (newArticlePage input errors))
    Right _ =>
      case validateArticle input of
        Left errors => pure (render context (newArticlePage input errors))
        Right valid => do
          insertArticle valid context
          pure (seeOther (pathTo showArticleRoute (MkArticlePath valid.slug)))

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

createArticleBinding : BoundRoute
createArticleBinding =
  handledBy createArticleRoute createArticle
```

The route declaration records the submitted body type, and `handledBy` checks
that the controller implements `ArticleForm -> ControllerContext ->
ControllerApp Response`.

## 8. Add Auth

Protect only the write path at first:

```idris
createArticle : ArticleForm -> ControllerContext -> ControllerApp Response
createArticle input context = do
  _ <- requireCurrentUser context
  case validateSessionCsrf context.session context.request of
    Left errors => pure (render context (newArticlePage input errors))
    Right _ =>
      case validateArticle input of
        Left errors => pure (render context (newArticlePage input errors))
        Right valid => do
          insertArticle valid context
          pure (seeOther (pathTo showArticleRoute (MkArticlePath valid.slug)))
```

Keep the auth decision in the handler. The route table remains a readable list
of HTTP method, path, and handler.

## 9. Add A Live Fragment

Mark the list as depending on the `articles` table:

```idris
articleFeed : ControllerContext -> List Article -> Html
articleFeed context articles =
  liveFragment context "article-feed" "/articles/partial" ["articles"]
    (articleList articles)
```

Use it in the full document:

```idris
articleIndexView : ControllerContext -> List Article -> Html
articleIndexView context articles =
  fragment
    [ <title>Articles</title>
    , <main id="main-content">
        {articleFeed context articles}
      </main>
    ]
```

Return the same region from a fragment endpoint:

```idris
articlesPartial : ControllerContext -> ControllerApp Response
articlesPartial context = do
  rows <-
    sqlQuery
      "select articles.* from articles order by created_at desc"
  pure (renderFragment context (articleFeed context rows))

articlesPartialRoute : RouteSpec NoInput NoInput Response
articlesPartialRoute =
  get "/articles/partial"

articlesPartialBinding : BoundRoute
articlesPartialBinding =
  handledBy articlesPartialRoute articlesPartial
```

Enable Auto Refresh once in the app runner:

```idris
main : IO ()
main =
  runApp
    (app "My App" appRoutes
      |> withDatabaseFromEnv
      |> withSessionSecretFromEnv
      |> withAutoRefresh)
```

The page says which table it depends on. Iwf handles the live refresh wiring and
refresh request.

## 10. Ship With Check

Keep the route table readable:

```idris
export
htmlArticlesRoute : RouteSpec NoInput NoInput Response
htmlArticlesRoute =
  get "/articles"

htmlArticlesBinding : BoundRoute
htmlArticlesBinding =
  handledBy htmlArticlesRoute articles

export
htmlNewArticleRoute : RouteSpec NoInput NoInput Response
htmlNewArticleRoute =
  get "/articles/new"

htmlNewArticleBinding : BoundRoute
htmlNewArticleBinding =
  handledBy htmlNewArticleRoute newArticle

export
htmlCreateArticleRoute : RouteSpec NoInput ArticleForm Response
htmlCreateArticleRoute =
  post "/articles" |> body ArticleForm |> html

htmlCreateArticleBinding : BoundRoute
htmlCreateArticleBinding =
  handledBy htmlCreateArticleRoute createArticle

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

htmlArticleBinding : BoundRoute
htmlArticleBinding =
  handledBy htmlArticleRoute showArticle

export
htmlArticlesPartialRoute : RouteSpec NoInput NoInput Response
htmlArticlesPartialRoute =
  get "/articles/partial"

htmlArticlesPartialBinding : BoundRoute
htmlArticlesPartialBinding =
  handledBy htmlArticlesPartialRoute articlesPartial

export
htmlRoutes : Routes
htmlRoutes =
  [ htmlArticlesBinding
  , htmlNewArticleBinding
  , htmlCreateArticleBinding
  , htmlArticleBinding
  , htmlArticlesPartialBinding
  ]

appRoutes : Routes
appRoutes =
  htmlRoutes
```

Run the app check before shipping:

```sh
iwf check
```

At this point the feature has direct page HTML, direct forms, declared route
records, checked SQL, validation, auth, and one live fragment without leaving
the app-facing interface.

## Next

Read [Architecture](architecture.md) when you want to split the single-file
starter into `Application/`, `Config/`, and `Web/` modules.