# Readability Review — darcsweb
## Summary
Overall the project reads well for a small Scotty-based web app: modules are
split by responsibility, the domain types live in one place, and the security-
sensitive helpers are isolated in `Clone.hs`/`Darcs.hs`. The biggest sources
of friction for a first-time reader are (1) deeply nested `if … then … else`
chains in `Main.hs` (`serveStatic`, `withRepo`, `serveClone`, `getRepoBlob`)
where guards or early-return helpers would flatten the control flow
dramatically, (2) long `renderXxx` functions in `Html.hs` that interleave
string concatenation, branching and escaping in one big `T.concat` block,
and (3) a sprinkling of partial functions (`head`, `init`, `last`, `read`,
`!!`) that force the reader to reason about totality. The Coq-extracted
modules in `gen/` are, as expected, painful to read but correctly marked
un-editable at the Haskell level.
## Confusing constructs
### `app/Main.hs`
- **`app/Main.hs:74`** — `foldl (flip id) defaultOpts o` is cute but opaque.
Current:
```haskell
(o, _, []) -> return (foldl (flip id) defaultOpts o)
```
Plain rewrite:
```haskell
(updates, _, []) -> return (foldr ($) defaultOpts updates)
-- or, even more explicit:
-- return (foldl (\opts f -> f opts) defaultOpts updates)
```
`foldr ($)` is the standard idiom for "apply each endomorphism in turn";
`flip id` hides the fact that the fold is just function application.
- **`app/Main.hs:105-120`** — The two branches of `if optDaemon opts` duplicate
almost the entire startup (logging, building the config, calling
`runServer`). A reader has to diff the two branches visually to see that
only the logger and the `withSyslog` wrapper differ. Extract:
```haskell
let startup logf wrap = wrap $ do
logf $ "Starting on " ++ bind ++ ":" ++ show port
logf $ "Serving repositories from: " ++ absRepoDir
runServer (mkConfig port bind absRepoDir title absStaticDir logf)
if optDaemon opts
then do
logStdout $ "Daemonizing (bind " ++ bind ++ ":" ++ show port ++ ")"
hFlush stdout
daemonize (withSyslog "darcsweb" [LogPID] Daemon (startup logSyslog id))
else startup logStdout id
```
- **`app/Main.hs:346-380`** — `serveStatic` is a 35-line cascade of five
nested `if … then … else` blocks, each with a duplicated 404 tail. Refactor
to a helper that returns `Either NotFound FilePath` and a single responder:
```haskell
serveStatic :: DarcsWebConfig -> ActionM ()
serveStatic cfg = do
req <- request
mFile <- liftIO (resolveStatic cfg (pathInfo req))
case mFile of
Nothing -> respond404 "Not found."
Just path -> do
setHeader "Content-Type" (mimeType (takeExtension path))
setHeader "Cache-Control" "public, max-age=86400, immutable"
file path
respond404 :: Text -> ActionM ()
respond404 msg = do
status status404
html $ TL.fromStrict $ render404 msg
```
`respond404` alone replaces six copy-pasted 2-line blocks across this
file (lines 242, 292, 306, 320, 333, 341, 358, 368, 375, 389, 396,
405, 438). This is probably the single biggest readability win in the
project.
- **`app/Main.hs:354-356`** — Three separate `any` predicates on the same
list, two of which overlap (`s == "."` and `T.isPrefixOf "."`).
Current:
```haskell
if null subSegments
|| any (\s -> s == ".." || s == "." || T.null s) subSegments
|| any (T.isPrefixOf ".") subSegments
```
Plain rewrite:
```haskell
let isUnsafe s = T.null s || s == ".." || T.isPrefixOf "." s
if null subSegments || any isUnsafe subSegments
```
(`T.isPrefixOf "."` already covers `s == "."`.)
- **`app/Main.hs:385-406`** — `withRepo` mixes name validation, repo
existence check, canonicalization, and jail check in one big guard-and-
nested-if. The guard on line 387-388 packs three predicates with awkward
operator precedence. Rewrite the guard as a named helper:
```haskell
isBadName :: Text -> Bool
isBadName n =
T.any (`elem` ("/\\" :: String)) n
|| T.isInfixOf ".." n
|| T.isPrefixOf "." n
```
then `withRepo` reads `| isBadName name = respond404 "Invalid repository name."`.
- **`app/Main.hs:413-414`** — `findRepo` reimplements `Data.List.find`:
```haskell
findRepo name = foldr (\r acc -> if riName r == name then Just r else acc) Nothing
```
Plain rewrite:
```haskell
import Data.List (find)
findRepo name = find ((== name) . riName)
```
- **`app/Main.hs:449-454`** — Point-free section hides intent:
```haskell
decodeHdr = (>>= eitherToMaybe . TE.decodeUtf8') . flip lookup hdrs
```
Plain rewrite:
```haskell
decodeHdr :: BS.ByteString -> Maybe Text
decodeHdr name = do
raw <- lookup name hdrs
either (const Nothing) Just (TE.decodeUtf8' raw)
```
One fewer combinator, one extra type signature, much clearer causal chain.
### `src/DarcsWeb/Clone.hs`
- **`src/DarcsWeb/Clone.hs:117-119`** — The list comprehension returns a
list of `Text`s and then `T.concat`s, which re-walks the bytestring:
```haskell
encodePathSegment t =
T.concat [ encodeByte b | b <- BS.unpack (TE.encodeUtf8 t) ]
```
Plain and equivalent:
```haskell
encodePathSegment t =
T.concat (map encodeByte (BS.unpack (TE.encodeUtf8 t)))
```
A trivial change, but it removes the one list-comprehension from this
module (the rest is `map`/`filter`/`case`), eliminating a stylistic bump.
- **`src/DarcsWeb/Clone.hs:122-124`** — The `Word8 -> Text` branch uses
`toEnum (fromIntegral b)` which is only safe because we already filtered
to unreserved ASCII. A reader has to verify that. A more obviously safe
form: `T.singleton (BC.head (BS.singleton b))` is worse; the clearer
fix is a comment or a named helper:
```haskell
-- safe: isUnreserved b implies b is an ASCII byte
word8ToChar :: Word8 -> Char
word8ToChar = toEnum . fromIntegral
```
and use `word8ToChar b` in both `isUnreserved` (which also does the same
conversion) and the `T.singleton` branch.
- **`src/DarcsWeb/Clone.hs:125-129`** — `isUnreserved` is defined inside
`encodeByte`'s `where` and does the `toEnum (fromIntegral b)` dance
again. Extract once (see previous bullet).
### `src/DarcsWeb/Darcs.hs`
- **`src/DarcsWeb/Darcs.hs:69-96`** — `checkRepo` has a ladder of three
nested `if … then … else` and duplicates the `RepoInfo` record
construction between the two `Just`/`Nothing` cases (only two fields
differ). Rewrite as a single early-exit style:
```haskell
checkRepo baseDir name = do
let fullPath = baseDir </> name
isDir <- doesDirectoryExist fullPath
isRepo <- if isDir then isDarcsRepo fullPath else pure False
if not isRepo
then pure []
else do
desc <- readRepoDescription fullPath
mInfo <- getBasicRepoInfo fullPath
let (lastDate, count) = maybe ("", 0) id mInfo
pure [ RepoInfo
{ riName = T.pack name
, riPath = fullPath
, riDescription = desc
, riLastChange = lastDate
, riPatchCount = count
} ]
```
(`fromMaybe ("", 0) mInfo` is even shorter.) The record literal appears
once, which means future fields can't drift between the branches.
- **`src/DarcsWeb/Darcs.hs:176-181`** — `jailCheck` re-implements trailing-slash
logic that already lives in `PathPure.add_trailing_slash`:
```haskell
let jailSlash = if null jail then "/"
else if last jail == '/' then jail else jail ++ "/"
return (jailSlash `isPrefixOf` canonical || canonical == init jailSlash)
```
Uses **partial** `last` and **partial** `init`. Both are safe only
because of the `null` guard and the fact that the string ends in `/`,
which forces the reader to trace the condition twice. Plain rewrite:
```haskell
jailCheck jail path = do
canonical <- canonicalizePath path
let jailSlash = PathPure.add_trailing_slash jail
jailNoSlash = dropSuffix "/" jailSlash
pure (jailSlash `isPrefixOf` canonical || canonical == jailNoSlash)
where
dropSuffix suf s
| suf `isSuffixOf` s = take (length s - length suf) s
| otherwise = s
```
Now there are no partial functions and the "is it the jail itself, or
inside the jail?" logic is a one-liner predicate each.
- **`src/DarcsWeb/Darcs.hs:141-144`, `252-272`** — Two `extractPatch*`
functions differ only in whether they render the diff. Collapse into
a parameterised helper:
```haskell
data DiffMode = WithDiff | ListingOnly
extractPatch :: RepoPatch p => DiffMode -> PatchInfoAnd p wA wB -> PatchSummary
extractPatch mode piap =
let pinfo = info piap
(diffText, summaryText) = case hopefullyM piap of
Just p -> ( case mode of
WithDiff -> T.pack (renderString (showPatch ForDisplay p))
ListingOnly -> ""
, T.pack (renderString (summary p)) )
Nothing -> (if mode == WithDiff then "(patch content unavailable)" else "", "")
in patchInfoToSummary pinfo diffText summaryText
```
Two callers, one function. If that feels over-engineered, at minimum
factor out the shared `case hopefullyM piap of Just _ -> … ; Nothing -> …`
idiom into a helper so the two definitions visually pair up.
### `src/DarcsWeb/Html.hs`
- **`src/DarcsWeb/Html.hs:274`** — `maybe (psName ps) id (psTagName ps)` is
`fromMaybe (psName ps) (psTagName ps)`. Preferred:
```haskell
import Data.Maybe (fromMaybe)
fromMaybe (psName ps) (psTagName ps)
```
- **`src/DarcsWeb/Html.hs:298-308`** — `buildCrumbs` is a recursive helper
that threads an accumulator. A reader has to follow two state updates
per recursion. A `scanl`/`zip`/`map` version reads as "build prefix paths,
then render each":
```haskell
renderTreeBreadcrumb repoName subPath =
let parts = if T.null subPath then [] else T.splitOn "/" subPath
paths = drop 1 (T.scanl joinSeg "" parts)
crumbs = zipWith crumb paths parts
crumb href label =
" / <a href=\"/repo/" <> esc repoName <> "/tree/" <> esc href <> "\">"
<> esc label <> "</a>"
joinSeg acc p = if T.null acc then p else acc <> "/" <> p
in "<div class=\"tree-path\">"
<> "<a href=\"/repo/" <> esc repoName <> "/tree\">[root]</a>"
<> T.concat crumbs
<> "</div>\n"
```
(Note: `T.scanl` works on chars, so use `Data.List.scanl` with the list.
The point stands: "paths, labels, zip, render" is easier to skim than
mutually recursive accumulator code.) The same helper is **duplicated**
in `renderBlobBreadcrumb` (line 367-381) with only the final `fileName`
line differing — extract once.
- **`src/DarcsWeb/Html.hs:431-445`** — `relativeDate` is a ladder of six
`if … then … else if …` branches. Haskell's `|` guards read much
better for this pattern:
```haskell
relativeDate now dateStr =
case parseDarcsDate (T.unpack dateStr) of
Nothing -> dateStr
Just t ->
let secs = floor (diffUTCTime now t) :: Int
in pickBucket secs
where
pickBucket s
| s < 0 = formatAbsolute dateStr
| s < 60 = pluralize s "second"
| s < 3600 = pluralize (s `div` 60) "minute"
| s < 86400 = pluralize (s `div` 3600) "hour"
| s < 604800 = pluralize (s `div` 86400) "day"
| s < 2419200 = pluralize (s `div` 604800) "week"
| otherwise = formatAbsolute dateStr
```
Bonus: name the magic numbers:
```haskell
minute, hour, day, week, month :: Int
minute = 60; hour = 60 * minute; day = 24 * hour
week = 7 * day; month = 4 * week
```
- **`src/DarcsWeb/Html.hs:419-425`** — `highlightDiff`'s three-branch cascade
is fine, but each branch builds the same `<span class="diff-X">…</span>\n`
shape. A data-driven version reads more symmetrically:
```haskell
highlightDiff = T.concat . map highlightLine . T.lines
where
highlightLine l = case classify l of
Just cls -> "<span class=\"" <> cls <> "\">" <> esc l <> "</span>\n"
Nothing -> esc l <> "\n"
classify l
| T.isPrefixOf "+" l = Just "diff-add"
| T.isPrefixOf "-" l = Just "diff-del"
| T.isPrefixOf "@@" l = Just "diff-hunk"
| otherwise = Nothing
```
- **`src/DarcsWeb/Html.hs:452-458`** — `formatAbsolute` uses string slicing
with `take`/`drop` offsets. It works but is tedious to audit. A splitAt
pipeline reads more naturally:
```haskell
formatAbsolute d
| T.length d >= 14 =
let (y, r1) = T.splitAt 4 d
(mo, r2) = T.splitAt 2 r1
(dy, r3) = T.splitAt 2 r2
(h, r4) = T.splitAt 2 r3
(mi, r5) = T.splitAt 2 r4
(se, _) = T.splitAt 2 r5
in y <> "-" <> mo <> "-" <> dy <> " " <> h <> ":" <> mi <> ":" <> se
| otherwise = d
```
(And stay in `Text`, avoiding the `T.unpack`/`T.pack` round-trip.)
- **`src/DarcsWeb/Html.hs:367-381`** — `renderBlobBreadcrumb` uses partial
`init` and `last` on `T.splitOn "/" subPath`. If `subPath` ever arrived
as `""`, both fail. Route guard should ensure it can't, but "readability
first" still prefers a total version:
```haskell
case T.splitOn "/" subPath of
[] -> "" -- impossible, but total
[fileName] -> renderWithFile [] fileName
parts -> renderWithFile (init parts) (last parts)
```
## Naming
- **`app/Main.hs:50-53`** — `Opts` is used only for parsed CLI flags. Rename
to `CliOpts` / `Flags` / `CliArgs` to avoid collision with
`Web.Scotty.Options` which is imported on the same file.
- **`app/Main.hs:96-100`** — Local bindings use abbreviated `cfgMap`-
extracted names: `port`, `bind`, `repoDir`, `title`, `staticDir`.
Good. But the record later uses `cfgPort`, `cfgBind`, `cfgRepoDir`,
`cfgTitle`, `cfgStaticDir` and the `mkConfig` parameter list on line 122
repeats the positional order. If one day the record gets a new field,
`mkConfig`'s 6-argument positional call site is a silent refactor hazard.
Prefer record syntax at the call site:
```haskell
let cfg = DarcsWebConfig { cfgPort = port, cfgBind = bind, ... cfgLog = logf }
```
and delete `mkConfig` entirely.
- **`app/Main.hs:113,116`** — `logf` locally and `cfgLog` on the record.
Pick one (`logf` throughout is fine).
- **`app/Main.hs:451`** — `hdrs` vs. `requestHeaders`. Project is generally
consistent on full names — `hdrs` is the one outlier.
- **`src/DarcsWeb/Clone.hs:37,40,41`** — `mProto`, `mHost`, `name`, then
locally `proto`, `host`. Fine, but `host`/`mHost` shadowing is confusing:
rename the local to `finalHost` or `hostOrDefault`.
- **`src/DarcsWeb/Clone.hs:63,64`** — `raw` / `h` / `h` / `p` single-letter
locals. `h` for both "host-like string" in `validRegName` and "name"
inside the where clause is reused. Consider `host`, `port`.
- **`src/DarcsWeb/Darcs.hs:107`** — `getBasicRepoInfo` returns
`Maybe (Text, Int)` — an anonymous tuple. A record (`data RepoStats =
RepoStats { rsLastChange :: !Text, rsPatchCount :: !Int }`) would
document what `fst`/`snd` mean at the call site (line 90).
- **`src/DarcsWeb/Darcs.hs:253-255,263-265`** — `extractPatchListing` vs.
`extractPatchFull`. "Listing" vs. "Full" is fine; better names could be
`summariseWithoutDiff` / `summariseWithDiff`, or see the `DiffMode`
refactor above.
- **`src/DarcsWeb/Html.hs:405-409`** — `navLink'` has a trailing prime
with no un-primed counterpart. Drop the prime: `navLink`.
- **`src/DarcsWeb/Html.hs:84`** — `"num"` CSS class is fine, but `T.pack
(show (riPatchCount ri))` appears three times in this module with
slightly different spelling. A one-liner helper `tshow = T.pack . show`
would cut noise.
## Structure
- **`app/Main.hs:217-342`** — `app` is ~125 lines of inline route
definitions. Each route repeats the shape `pathParam …; withRepo cfg
name $ \repoPath -> do …`. Consider:
1. Extract each handler (`handleSummary`, `handleShortlog`, `handleLog`,
`handleTags`, `handleTree`, `handleBlob`, `handlePatch`) to a named
top-level function with a type signature. `app` then becomes a
one-screen route table.
2. Collapse the common "lookup optional value + 404-or-render" pattern
(lines 290-295, 304-309, 318-323, 331-337) into a helper:
```haskell
renderOr404 :: Text -> Maybe a -> (a -> Text) -> ActionM ()
renderOr404 msg mVal render = case mVal of
Nothing -> respond404 msg
Just x -> html (TL.fromStrict (render x))
```
- **`app/Main.hs:6-35`** — The import list for Main spans 30 lines and
mixes `Web.Scotty`, `Network.Wai`, POSIX, FFI, `Data.Text.*`, `System.*`.
Grouping already helps; adding a blank line between `System.Posix.*`
and `Foreign.*` would signal "FFI section" and a comment
`-- Daemonization (POSIX + FFI)` on line 28 would frame why the FFI is
there.
- **`app/Main.hs:169-176`** — `openDevNull` uses the raw `2` for `O_RDWR`.
Either import from `System.Posix.IO` (`OpenMode(..)`) or at least name
the constant: `let o_RDWR = 2 in …`. Also, a comment already explains
*why* (unix-package compat); move it to a Haddock on `openDevNull`
itself so it sticks to the function.
- **`src/DarcsWeb/Html.hs`** — At 468 lines, this module mixes:
- page chrome (`renderPage`, `repoBreadcrumb`, `repoNavBar`, `navLink'`)
- list renderers (`renderRepoList`, `renderRepoTable`, `renderRepoRow`,
`renderShortLogTable`/`Row`, `renderTagList`/`Row`)
- entity pages (`renderRepoSummary`, `renderPatchDetail`, `renderTree`,
`renderBlob`, `render404`)
- text utilities (`esc`, `highlightDiff`, `shortAuthor`, `formatSize`,
`formatAbsolute`, `relativeDate`, `parseDarcsDate`, `pluralize`)
Splitting into `DarcsWeb.Html.Page`, `DarcsWeb.Html.Repo`,
`DarcsWeb.Html.Patch`, `DarcsWeb.Html.Format` would let a reader
navigate by responsibility. If a split is too invasive, at minimum
add banner comments (`-- * Page chrome`, `-- * Log views`, …) so
the TOC is visible when scrolling.
- **`src/DarcsWeb/Darcs.hs:106-148`** — `getBasicRepoInfo`,
`getRepoPatches`, `getRepoPatch`, `getRepoTags` all share the exact
`try $ withRepositoryLocation YesUseCache repoPath $ RepoJob $ \r -> …`
scaffolding plus a `case … of Left _ -> empty; Right v -> v` unwrap.
Extract:
```haskell
withRepoSafe :: a -> FilePath
-> (forall p wR. RepoPatch p => Repository … -> IO a)
-> IO a
withRepoSafe fallback path job = do
r <- try $ withRepositoryLocation YesUseCache path (RepoJob job)
pure $ case r of Left (_ :: SomeException) -> fallback; Right v -> v
```
The four call sites shrink to 3 lines each and the exception-handling
policy lives in one place.
- **`src/DarcsWeb/Config.hs:33`** — `trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace`
is a classic but surprising one-liner for non-Haskellers. `Data.Text`
has `T.strip` for `Text`; for `String` the equivalent one-liner is
acceptable but a `where` binding with a short comment would help
first-time readers.
## Comments & docs
- **`app/Main.hs:1-2`** — No module-level Haddock describing what Main does.
Three lines would help:
```haskell
-- | darcsweb executable: parses CLI flags, loads config, optionally
-- daemonizes via a double-fork, and starts a Scotty server that
-- serves repository pages and read-only clone files.
```
- **`app/Main.hs:150-159`** — `daemonize` has a one-line comment but no
explanation of *why* the double-fork is needed (SysV-style disown from
controlling terminal). One line would save the next maintainer a
Stack Overflow detour:
```haskell
-- | Double-fork: first fork + setsid() detaches from the controlling
-- terminal; second fork ensures we are not a session leader, so we
-- can never re-acquire a TTY.
```
- **`app/Main.hs:408-411`** — The Haddock says "uses formally verified
implementation from Coq/Rocq" — good pointer, but a link (or mention
of `verified/Path.v`) would make the trail explicit.
- **`src/DarcsWeb/Clone.hs:3-31`** — Excellent Haddock on `buildCloneUrl`.
`sanitizeHost`, `validAuthority`, `validBracketed`, `validRegName` would
benefit from matching `@since`/spec-style annotations noting RFC 3986
sections they partially implement.
- **`src/DarcsWeb/Darcs.hs:174-181`** — `jailCheck` has a comment but no
Haddock. Since this function is a critical security boundary (reused
in three places), it should be documented properly:
```haskell
-- | Return 'True' iff 'path', after symlink resolution, is either the
-- 'jail' directory itself or a strict descendant of it. Used to
-- prevent path traversal through symlinks.
```
- **`src/DarcsWeb/Html.hs:298-308,367-381`** — No Haddock on breadcrumb
helpers. Since the two are near-duplicates, docs should either explain
the difference or (preferable) factor them.
- **`test/Properties/Clone.hs`**, **`test/Properties/Csp.hs`**,
**`test/Properties/Html.hs`** — Tests are consistently formatted and
readable. The `run`/`quickCheckWithResult` boilerplate is duplicated
across all three — worth extracting to a shared `Properties.Runner`
module with one `runProp :: Testable p => String -> p -> IO Bool`.
## Small wins
Ordered by impact:
1. **`respond404` helper in `app/Main.hs`.** Kills ~13 duplicated 2-line
blocks (`app/Main.hs:242-243, 292-293, 306-307, 320-321, 333-334, 341-342,
358-359, 368-369, 374-375, 389-390, 396-397, 405-406, 438-440`).
2. **Replace `findRepo` body with `find`** (`app/Main.hs:414`).
3. **Replace `maybe X id` with `fromMaybe X`** (`src/DarcsWeb/Html.hs:274`).
4. **Replace `foldl (flip id)` with `foldr ($)`** (`app/Main.hs:74`).
5. **Drop `mkConfig`; use record syntax inline** (`app/Main.hs:113, 119, 122`).
6. **Top-level type signatures on inner `where` helpers** —
`app/Main.hs:453` (`eitherToMaybe`), `src/DarcsWeb/Html.hs:444`
(`pluralize`). They're short but the types aren't obvious.
7. **Guards instead of nested `if/else`** — `src/DarcsWeb/Html.hs:431-445`,
`app/Main.hs:354-359`, `src/DarcsWeb/Darcs.hs:196-213`.
8. **Blank-line-grouped imports** with `-- Scotty`, `-- WAI`,
`-- POSIX / FFI`, `-- Local modules` section comments
(`app/Main.hs:6-43`).
9. **`tshow = T.pack . show`** in `src/DarcsWeb/Html.hs` — removes 6
noisy repetitions (`Html.hs:84, 349, 350, 351, 445`).
10. **Rename `navLink'` to `navLink`** (`src/DarcsWeb/Html.hs:405`) — no
un-primed sibling, the tick carries no information.
11. **`darcsDir` is only used twice in Main** (`app/Main.hs:47, 423`). Fine
to keep, but add the same constant in `src/DarcsWeb/Darcs.hs` rather
than the bare string `"_darcs"` (appears at lines 60, 100, 209).
Either push `darcsDir` into `Types.hs` or introduce
`DarcsWeb.Internal.Constants`.
12. **`Data.List (isPrefixOf)`** is imported in `app/Main.hs:35` and used
once (line 367). Paired with the similar import in `Darcs.hs:23` and
the verified `PathPure.add_trailing_slash` call, a single
`pathIsInside :: FilePath -> FilePath -> Bool` helper (in `PathPure`
or in a thin wrapper) would be clearer and testable.
## Extracted code note
Files `gen/CspPure.hs`, `gen/HtmlPure.hs`, `gen/PathPure.hs` are Coq
extraction output. They exhibit the usual extraction accents:
- **`gen/CspPure.hs:9-16`** — Hand-rolled `fst`/`snd` shadowing `Prelude`.
Extraction-generated; harmless because `{-# OPTIONS_GHC -w #-}` silences
the shadow warning. **Un-editable at source**. If the Coq side can
map its tuple projections to the standard ones (via
`Extract Constant fst => "Prelude.fst".`), the extracted file would
read better. Same applies to `map` on line 18-22.
- **`gen/CspPure.hs:29-31`**, **`gen/HtmlPure.hs:18-35`**,
**`gen/PathPure.hs:19-21, 44-46, 79-89`** — Every character comparison
is annotated with
`((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)`. This
is an extraction artefact (Coq's decidable equality realisation). A
Coq-side `Extract Inductive bool => "Prelude.Bool" …` and
`Extract Inlined Constant Char.eqb => "(Prelude.==)"` would remove the
inline type ascriptions and drop ~30% of the visual noise. **Un-editable
at source**.
- **`gen/HtmlPure.hs:9-10`**, **`gen/HtmlPure.hs:13-14`** — Identity lambdas
`(\x -> x) '"'` are obfuscated literals. Extraction-generated; in Coq,
defining `Definition dquote := "034"%char` (or simply inlining the
literal) and marking it `Extract Constant dquote => "'\"'"` would
produce readable Haskell. **Un-editable at source**.
- **`gen/PathPure.hs:70-90`** — `is_safe_segment` is a four-deep nested
`(Prelude.&&)` tower. This is the natural result of extracting a
conjunction of `bool` predicates. If the Coq definition switched to a
`forallb` over a list of unary predicates (or used `&&&`-style local
notation), the extract would read better. **Un-editable at source**.
- **`gen/PathPure.hs:1-3`**, **`gen/HtmlPure.hs:1-3`**,
**`gen/CspPure.hs:1-3`** — All three extracts import `Data.Bits` and
`Data.Char` unconditionally, though none reference them. Extraction
artefact. **Un-editable at source**; can only be suppressed via
`-Wno-unused-imports` (already implicit under `-w`).
**Wrapper-side improvements (editable):** the thin Haskell wrappers in
`src/DarcsWeb/Html.hs:414`, `src/DarcsWeb/Darcs.hs:186, 191`,
`app/Main.hs:411`, `app/Main.hs:195` are all one-liners that call through
to the extracted `HtmlPure` / `PathPure` / `CspPure` module. They are the
right place to add Haddock with a link to the corresponding `.v` proof
file (e.g. `-- See @verified/Html.v@ for the proof that this is
HTML-injection safe.`) so the reader immediately knows where to look for
the semantic guarantee instead of having to pattern-match the mangled
extracted source.
