|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | + |
| 3 | +/// PanLL StrategyDrift Component — visualises the learning loop's |
| 4 | +/// top-prover-per-class recommendations, the PROVEN/SANCTIFY certificate |
| 5 | +/// landscape, and strategy-shift events. |
| 6 | +/// |
| 7 | +/// Data sources (all polled on a timer): |
| 8 | +/// GET http://localhost:8080/api/v1/proof_attempts/certificates |
| 9 | +/// GET http://localhost:8080/api/v1/proof_attempts/coverage |
| 10 | +/// Hypatia.Rules.StrategyDrift.snapshot/0 (via HTTP bridge — TODO) |
| 11 | +/// |
| 12 | +/// Layout: three stacked panels |
| 13 | +/// 1. Certs Grid — 11 classes × N provers, cert-status colouring |
| 14 | +/// 2. Coverage Bars — per-class n_repos × n_provers × n_attempts |
| 15 | +/// 3. Drift Events — append-only log of shift events |
| 16 | + |
| 17 | +open Tea.Html |
| 18 | + |
| 19 | +// ── Shared types ─────────────────────────────────────────────────────── |
| 20 | + |
| 21 | +type certStatus = Proven | Pending | Sanctified | Unknown |
| 22 | + |
| 23 | +type proverCert = { |
| 24 | + obligation_class: string, |
| 25 | + prover_used: string, |
| 26 | + success_rate: float, |
| 27 | + total_attempts: int, |
| 28 | + status: certStatus, |
| 29 | +} |
| 30 | + |
| 31 | +type classCoverage = { |
| 32 | + obligation_class: string, |
| 33 | + n_repos: int, |
| 34 | + n_provers: int, |
| 35 | + n_attempts: int, |
| 36 | + n_success: int, |
| 37 | +} |
| 38 | + |
| 39 | +type driftEvent = { |
| 40 | + timestamp: string, |
| 41 | + obligation_class: string, |
| 42 | + old_top: string, |
| 43 | + new_top: string, |
| 44 | + candidates_requeued: int, |
| 45 | +} |
| 46 | + |
| 47 | +type strategyDriftModel = { |
| 48 | + certs: array<proverCert>, |
| 49 | + coverage: array<classCoverage>, |
| 50 | + drift_events: array<driftEvent>, |
| 51 | + last_refresh: string, |
| 52 | + error: option<string>, |
| 53 | +} |
| 54 | + |
| 55 | +// ── Render helpers ───────────────────────────────────────────────────── |
| 56 | + |
| 57 | +let statusBadge = (status: certStatus): Tea_Vdom.t<'msg> => { |
| 58 | + let (color, label) = switch status { |
| 59 | + | Proven => ("text-green-400 border-green-500", "PROVEN") |
| 60 | + | Sanctified => ("text-amber-300 border-amber-400 border-2", "SANCTIFIED") |
| 61 | + | Pending => ("text-gray-400 border-gray-600", "pending") |
| 62 | + | Unknown => ("text-gray-500 border-gray-700", "?") |
| 63 | + } |
| 64 | + span( |
| 65 | + list{Attrs.class_("inline-block px-2 py-1 text-xs font-mono border " ++ color)}, |
| 66 | + list{text(label)}, |
| 67 | + ) |
| 68 | +} |
| 69 | + |
| 70 | +let certCell = (cert: proverCert): Tea_Vdom.t<'msg> => { |
| 71 | + let rate_pct = Js.Float.toFixedWithPrecision(cert.success_rate *. 100.0, ~digits=0) |
| 72 | + let intensity = if cert.success_rate > 0.9 { |
| 73 | + "bg-green-900/40" |
| 74 | + } else if cert.success_rate > 0.5 { |
| 75 | + "bg-yellow-900/40" |
| 76 | + } else { |
| 77 | + "bg-red-900/40" |
| 78 | + } |
| 79 | + div( |
| 80 | + list{Attrs.class_("p-2 border border-gray-700 " ++ intensity)}, |
| 81 | + list{ |
| 82 | + div( |
| 83 | + list{Attrs.class_("text-sm font-mono text-gray-200")}, |
| 84 | + list{text(cert.prover_used)}, |
| 85 | + ), |
| 86 | + div( |
| 87 | + list{Attrs.class_("text-xs font-mono text-gray-400")}, |
| 88 | + list{text(rate_pct ++ "% · n=" ++ Belt.Int.toString(cert.total_attempts))}, |
| 89 | + ), |
| 90 | + statusBadge(cert.status), |
| 91 | + }, |
| 92 | + ) |
| 93 | +} |
| 94 | + |
| 95 | +let certsGrid = (certs: array<proverCert>): Tea_Vdom.t<'msg> => { |
| 96 | + let grouped = Belt.Array.reduce(certs, Js.Dict.empty(), (acc, cert) => { |
| 97 | + let key = cert.obligation_class |
| 98 | + let existing = switch Js.Dict.get(acc, key) { |
| 99 | + | Some(arr) => arr |
| 100 | + | None => [] |
| 101 | + } |
| 102 | + Js.Dict.set(acc, key, Belt.Array.concat(existing, [cert])) |
| 103 | + acc |
| 104 | + }) |
| 105 | + let classes = Js.Dict.keys(grouped) |
| 106 | + |
| 107 | + div( |
| 108 | + list{Attrs.class_("mb-4")}, |
| 109 | + list{ |
| 110 | + h3( |
| 111 | + list{Attrs.class_("text-lg font-bold text-gray-200 mb-2")}, |
| 112 | + list{text("Certificates Grid")}, |
| 113 | + ), |
| 114 | + div( |
| 115 | + list{Attrs.class_("space-y-2")}, |
| 116 | + Belt.Array.map(classes, class_name => { |
| 117 | + let class_certs = switch Js.Dict.get(grouped, class_name) { |
| 118 | + | Some(arr) => arr |
| 119 | + | None => [] |
| 120 | + } |
| 121 | + div( |
| 122 | + list{Attrs.class_("border-l-2 border-blue-500 pl-2")}, |
| 123 | + list{ |
| 124 | + div( |
| 125 | + list{Attrs.class_("text-sm font-mono text-gray-300 mb-1")}, |
| 126 | + list{text(class_name)}, |
| 127 | + ), |
| 128 | + div( |
| 129 | + list{Attrs.class_("flex gap-2 flex-wrap")}, |
| 130 | + Belt.Array.map(class_certs, certCell)->Belt.List.fromArray, |
| 131 | + ), |
| 132 | + }, |
| 133 | + ) |
| 134 | + })->Belt.List.fromArray, |
| 135 | + ), |
| 136 | + }, |
| 137 | + ) |
| 138 | +} |
| 139 | + |
| 140 | +let coverageBar = (cov: classCoverage): Tea_Vdom.t<'msg> => { |
| 141 | + let bar_width = Js.Math.min_int(cov.n_attempts * 2, 400) |
| 142 | + let bar_width_str = Belt.Int.toString(bar_width) ++ "px" |
| 143 | + div( |
| 144 | + list{Attrs.class_("flex items-center gap-3 py-1")}, |
| 145 | + list{ |
| 146 | + span( |
| 147 | + list{Attrs.class_("text-xs font-mono text-gray-400 w-24")}, |
| 148 | + list{text(cov.obligation_class)}, |
| 149 | + ), |
| 150 | + div( |
| 151 | + list{ |
| 152 | + Attrs.class_("h-4 bg-blue-900/60 border border-blue-700"), |
| 153 | + Attrs.style("width", bar_width_str), |
| 154 | + }, |
| 155 | + list{}, |
| 156 | + ), |
| 157 | + span( |
| 158 | + list{Attrs.class_("text-xs font-mono text-gray-400")}, |
| 159 | + list{ |
| 160 | + text( |
| 161 | + "n=" ++ |
| 162 | + Belt.Int.toString(cov.n_attempts) ++ |
| 163 | + " · " ++ |
| 164 | + Belt.Int.toString(cov.n_repos) ++ |
| 165 | + " repos · " ++ |
| 166 | + Belt.Int.toString(cov.n_provers) ++ |
| 167 | + " provers", |
| 168 | + ), |
| 169 | + }, |
| 170 | + ), |
| 171 | + }, |
| 172 | + ) |
| 173 | +} |
| 174 | + |
| 175 | +let coverageBars = (coverage: array<classCoverage>): Tea_Vdom.t<'msg> => { |
| 176 | + div( |
| 177 | + list{Attrs.class_("mb-4")}, |
| 178 | + list{ |
| 179 | + h3( |
| 180 | + list{Attrs.class_("text-lg font-bold text-gray-200 mb-2")}, |
| 181 | + list{text("Cross-Repo Coverage")}, |
| 182 | + ), |
| 183 | + div(list{Attrs.class_("space-y-1")}, Belt.Array.map(coverage, coverageBar)->Belt.List.fromArray), |
| 184 | + }, |
| 185 | + ) |
| 186 | +} |
| 187 | + |
| 188 | +let driftEventRow = (event: driftEvent): Tea_Vdom.t<'msg> => { |
| 189 | + div( |
| 190 | + list{Attrs.class_("flex gap-3 py-1 text-xs font-mono border-b border-gray-800")}, |
| 191 | + list{ |
| 192 | + span(list{Attrs.class_("text-gray-500 w-40")}, list{text(event.timestamp)}), |
| 193 | + span(list{Attrs.class_("text-blue-300 w-24")}, list{text(event.obligation_class)}), |
| 194 | + span( |
| 195 | + list{Attrs.class_("text-gray-400")}, |
| 196 | + list{text(event.old_top ++ " → ")}, |
| 197 | + ), |
| 198 | + span(list{Attrs.class_("text-green-400")}, list{text(event.new_top)}), |
| 199 | + span( |
| 200 | + list{Attrs.class_("text-amber-300 ml-auto")}, |
| 201 | + list{ |
| 202 | + text("re-queued " ++ Belt.Int.toString(event.candidates_requeued)), |
| 203 | + }, |
| 204 | + ), |
| 205 | + }, |
| 206 | + ) |
| 207 | +} |
| 208 | + |
| 209 | +let driftEventsPanel = (events: array<driftEvent>): Tea_Vdom.t<'msg> => { |
| 210 | + div( |
| 211 | + list{}, |
| 212 | + list{ |
| 213 | + h3( |
| 214 | + list{Attrs.class_("text-lg font-bold text-gray-200 mb-2")}, |
| 215 | + list{text("Strategy Drift Events")}, |
| 216 | + ), |
| 217 | + if Array.length(events) == 0 { |
| 218 | + div( |
| 219 | + list{Attrs.class_("text-sm text-gray-500 italic")}, |
| 220 | + list{text("No shifts detected yet.")}, |
| 221 | + ) |
| 222 | + } else { |
| 223 | + div(list{Attrs.class_("space-y-0")}, Belt.Array.map(events, driftEventRow)->Belt.List.fromArray) |
| 224 | + }, |
| 225 | + }, |
| 226 | + ) |
| 227 | +} |
| 228 | + |
| 229 | +// ── Top-level view ───────────────────────────────────────────────────── |
| 230 | + |
| 231 | +let view = (model: strategyDriftModel): Tea_Vdom.t<'msg> => { |
| 232 | + div( |
| 233 | + list{Attrs.class_("strategy-drift-panel p-4 bg-gray-900 text-gray-200 min-h-full")}, |
| 234 | + list{ |
| 235 | + div( |
| 236 | + list{Attrs.class_("flex items-baseline justify-between mb-4")}, |
| 237 | + list{ |
| 238 | + h2( |
| 239 | + list{Attrs.class_("text-xl font-bold")}, |
| 240 | + list{text("Strategy Drift")}, |
| 241 | + ), |
| 242 | + span( |
| 243 | + list{Attrs.class_("text-xs font-mono text-gray-500")}, |
| 244 | + list{text("refreshed: " ++ model.last_refresh)}, |
| 245 | + ), |
| 246 | + }, |
| 247 | + ), |
| 248 | + switch model.error { |
| 249 | + | Some(err) => |
| 250 | + div( |
| 251 | + list{Attrs.class_("mb-4 p-2 border border-red-700 bg-red-900/40 text-red-300 text-xs")}, |
| 252 | + list{text("error: " ++ err)}, |
| 253 | + ) |
| 254 | + | None => noNode |
| 255 | + }, |
| 256 | + certsGrid(model.certs), |
| 257 | + coverageBars(model.coverage), |
| 258 | + driftEventsPanel(model.drift_events), |
| 259 | + }, |
| 260 | + ) |
| 261 | +} |
| 262 | + |
| 263 | +// ── Decoders (JSON from verisim-api) ─────────────────────────────────── |
| 264 | + |
| 265 | +let certStatusOfString = (s: string): certStatus => { |
| 266 | + switch s { |
| 267 | + | "proven" => Proven |
| 268 | + | "sanctified" => Sanctified |
| 269 | + | "pending" => Pending |
| 270 | + | _ => Unknown |
| 271 | + } |
| 272 | +} |
0 commit comments