Skip to content

Commit 0c4566d

Browse files
committed
Merge branch 'main' of https://github.com/herbie-fp/odyssey
2 parents 6629631 + 673dacb commit 0c4566d

File tree

8 files changed

+374
-18
lines changed

8 files changed

+374
-18
lines changed

package-lock.json

Lines changed: 2 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

package.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@
8888
"react": "^18.2.0",
8989
"react-button-component": "^1.0.0",
9090
"react-debounce-input": "^3.3.0",
91-
"react-dom": "^18.2.0",
91+
"react-dom": "^18.3.1",
9292
"react-error-boundary": "^6.0.0",
9393
"react-icons": "^5.5.0",
9494
"react-latex-next": "^2.2.0",

src/herbie/DerivationComponent.tsx

Lines changed: 311 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,308 @@
11
import Latex from 'react-latex-next';
22
import * as HerbieContext from './HerbieContext';
33
import './DerivationComponent.css';
4+
import { ReactNode, useEffect } from 'react';
5+
import { DerivationNode, ProofStep } from './HerbieTypes';
6+
7+
// Function to convert FPCore to TeX (simplified version)
8+
function fpCoreToTeX(expr: string, options?: { loc: any; color: any; }) {
9+
// Handle colored output for specific locations if provided
10+
if (options && options.loc && options.loc.length > 0 && options.color) {
11+
// This is a simplified approach - a real implementation would navigate to the specific location
12+
// and wrap just that part in color
13+
return `\\color{${options.color}}{${
14+
expr
15+
.replace(/\(FPCore \(x\)\s+/g, '')
16+
.replace(/\)\)/g, '}')
17+
.replace(/\(\-\.f64/g, '(')
18+
.replace(/\(\+\.f64/g, '(')
19+
.replace(/\(\/\.f64/g, '\\frac{')
20+
.replace(/\(sqrt\.f64 \(\+\.f64 x 1\)\)/g, '\\sqrt{x + 1}')
21+
.replace(/\(sqrt\.f64 \(\+\.f64 1 x\)\)/g, '\\sqrt{1 + x}')
22+
.replace(/\(sqrt\.f64 x\)/g, '\\sqrt{x}')
23+
.replace(/\#s\(approx \(- \(\+ 1 x\) x\) 1\)/g, '1')
24+
.replace(/\(\+\.f64 1 x\)/g, '(1 + x)')
25+
}}`;
26+
}
27+
28+
// Basic conversion (highly simplified)
29+
return expr
30+
.replace(/\(FPCore \(x\)\s+/g, '')
31+
.replace(/\)\)/g, '}')
32+
.replace(/\(\-\.f64/g, '(')
33+
.replace(/\(\+\.f64/g, '(')
34+
.replace(/\(\/\.f64/g, '\\frac{')
35+
.replace(/\(sqrt\.f64 \(\+\.f64 x 1\)\)/g, '\\sqrt{x + 1}')
36+
.replace(/\(sqrt\.f64 \(\+\.f64 1 x\)\)/g, '\\sqrt{1 + x}')
37+
.replace(/\(sqrt\.f64 x\)/g, '\\sqrt{x}')
38+
.replace(/\#s\(approx \(- \(\+ 1 x\) x\) 1\)/g, '1')
39+
.replace(/\(\+\.f64 1 x\)/g, '(1 + x)');
40+
}
41+
42+
// Format accuracy for display
43+
function formatAccuracy(val: number, bits = null, unit = '%') {
44+
return typeof val === 'number' ? val.toFixed(1) + unit : val;
45+
}
46+
47+
// Render a proof to HTML
48+
function renderProof(proof: ProofStep[], options = {}) {
49+
const proofSteps = proof
50+
.filter(step => step.direction !== "goal")
51+
.map(step => {
52+
// Convert direction to human-readable form
53+
const dirText = step.direction === "rtl" ? "right to left" :
54+
step.direction === "ltr" ? "left to right" : "";
55+
56+
// Format error
57+
const err = step.error;
58+
59+
return (
60+
<li key={step.rule + Math.random()}>
61+
<p>
62+
<code title={dirText}>{step.rule}</code>
63+
<span className="error">{err}</span>
64+
</p>
65+
<div className="math" dangerouslySetInnerHTML={{
66+
__html: `\\[\\leadsto ${fpCoreToTeX(step.program, {
67+
loc: step.loc,
68+
color: "blue"
69+
})}\\]`
70+
}} />
71+
</li>
72+
);
73+
});
74+
75+
return (
76+
<li>
77+
<div className="proof">
78+
<details>
79+
<summary>Step-by-step derivation</summary>
80+
<ol>{proofSteps}</ol>
81+
</details>
82+
</div>
83+
</li>
84+
);
85+
}
86+
87+
88+
// Render history recursively
89+
function renderHistory(altn: DerivationNode, options = {}): ReactNode[] {
90+
const items = [];
91+
92+
if (altn.type === "start") {
93+
// Initial program
94+
const err = formatAccuracy(altn.error);
95+
const err2 = formatAccuracy(altn["training-error"]);
96+
97+
items.push(
98+
<li key="start">
99+
<p>
100+
Initial program <span className="error" title={`${err2} on training set`}>{err}</span>
101+
</p>
102+
<div className="math" dangerouslySetInnerHTML={{
103+
__html: `\\[${fpCoreToTeX(altn.program)}\\]`
104+
}} />
105+
</li>
106+
);
107+
}
108+
else if (altn.type === "add-preprocessing") {
109+
// Add the previous items if they exist
110+
if (altn.prev) {
111+
items.push(...renderHistory(altn.prev, options));
112+
}
113+
114+
// Add the preprocessing step
115+
items.push(<li key="preprocess">Add Preprocessing</li>);
116+
}
117+
else if (altn.type === "taylor") {
118+
// Add the previous items
119+
if (altn.prev) {
120+
items.push(...renderHistory(altn.prev, options));
121+
}
122+
123+
// Add Taylor expansion step
124+
items.push(
125+
<li key="taylor">
126+
<p>Taylor expanded in {altn.var} around {altn.pt}</p>
127+
<div className="math" dangerouslySetInnerHTML={{
128+
__html: `\\[\\leadsto ${fpCoreToTeX(altn.program, {
129+
loc: altn.loc,
130+
color: "blue"
131+
})}\\]`
132+
}} />
133+
</li>
134+
);
135+
}
136+
else if (altn.type === "rr") {
137+
// Add the previous items
138+
if (altn.prev) {
139+
items.push(...renderHistory(altn.prev, options));
140+
}
141+
142+
// Add proof if it exists
143+
if (altn.proof && altn.proof.length > 0) {
144+
items.push(renderProof(altn.proof, options));
145+
}
146+
147+
// Add rewrite rule application step
148+
const err = formatAccuracy(altn.error);
149+
const err2 = formatAccuracy(altn["training-error"]);
150+
151+
items.push(
152+
<li key="rr">
153+
<p>
154+
Applied rewrites<span className="error" title={`${err2} on training set`}>{err}</span>
155+
</p>
156+
<div className="math" dangerouslySetInnerHTML={{
157+
__html: `\\[\\leadsto ${fpCoreToTeX(altn.program, {
158+
loc: altn.loc,
159+
color: "blue"
160+
})}\\]`
161+
}} />
162+
</li>
163+
);
164+
}
165+
166+
return items;
167+
}
168+
169+
// Main component for rendering derivations
170+
const DerivationRenderer = (derivation: DerivationNode) => {
171+
// Load MathJax
172+
useEffect(() => {
173+
const script = document.createElement('script');
174+
script.src = 'https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=TeX-AMS_HTML';
175+
script.async = true;
176+
document.body.appendChild(script);
177+
178+
return () => {
179+
document.body.removeChild(script);
180+
};
181+
}, []);
182+
183+
184+
// // Example JSON data
185+
// const exampleDerivation: DerivationNode = {
186+
// "error": 0.16362048906511412,
187+
// "preprocessing": [],
188+
// "prev": {
189+
// "error": 0.16362048906511412,
190+
// "loc": [1],
191+
// "prev": {
192+
// "error": "N/A",
193+
// "loc": [1],
194+
// "prev": {
195+
// "error": 29.28147582053326,
196+
// "loc": [],
197+
// "prev": {
198+
// "error": 29.900400659788048,
199+
// "preprocessing": [],
200+
// "prev": {
201+
// "error": 29.900400659788048,
202+
// "program": "(FPCore (x) (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)))",
203+
// "training-error": 29.900400659788048,
204+
// "type": "start"
205+
// },
206+
// "program": "(FPCore (x) (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)))",
207+
// "training-error": 29.900400659788048,
208+
// "type": "add-preprocessing"
209+
// },
210+
// "program": "(FPCore (x)\n (/.f64 (-.f64 (+.f64 1 x) x) (+.f64 (sqrt.f64 x) (sqrt.f64 (+.f64 1 x)))))",
211+
// "proof": [
212+
// {
213+
// "direction": "goal",
214+
// "error": 29.900400659788048,
215+
// "loc": [],
216+
// "program": "(FPCore (x) (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)))",
217+
// "rule": "#f",
218+
// "tag": " ↑ 0 ↓ 0"
219+
// },
220+
// {
221+
// "direction": "ltr",
222+
// "error": "N/A",
223+
// "loc": [],
224+
// "program": "(FPCore (x) (- (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)))",
225+
// "rule": "lift--.f64",
226+
// "tag": " ↑ N/A ↓ N/A"
227+
// },
228+
// {
229+
// "direction": "ltr",
230+
// "error": "N/A",
231+
// "loc": [],
232+
// "program": "(FPCore (x)\n (/\n (-\n (* (sqrt.f64 (+.f64 x 1)) (sqrt.f64 (+.f64 x 1)))\n (* (sqrt.f64 x) (sqrt.f64 x)))\n (+ (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x))))",
233+
// "rule": "flip--",
234+
// "tag": " ↑ N/A ↓ N/A"
235+
// }
236+
// ],
237+
// "training-error": 29.28147582053326,
238+
// "type": "rr"
239+
// },
240+
// "program": "(FPCore (x) (/.f64 1 (+.f64 (sqrt.f64 x) (sqrt.f64 (+.f64 1 x)))))",
241+
// "pt": "0",
242+
// "training-error": "N/A",
243+
// "type": "taylor",
244+
// "var": "x"
245+
// },
246+
// "program": "(FPCore (x)\n (/.f64\n #s(approx (- (+ 1 x) x) 1)\n (+.f64 (sqrt.f64 x) (sqrt.f64 (+.f64 1 x)))))",
247+
// "proof": [
248+
// {
249+
// "direction": "goal",
250+
// "error": 0.16362048906511412,
251+
// "loc": [],
252+
// "program": "(FPCore (x) (/.f64 1 (+.f64 (sqrt.f64 x) (sqrt.f64 (+.f64 1 x)))))",
253+
// "rule": "#f",
254+
// "tag": " ↑ 0 ↓ 0"
255+
// }
256+
// ],
257+
// "training-error": 0.16362048906511412,
258+
// "type": "rr"
259+
// },
260+
// "program": "(FPCore (x)\n (/.f64\n #s(approx (- (+ 1 x) x) 1)\n (+.f64 (sqrt.f64 x) (sqrt.f64 (+.f64 1 x)))))",
261+
// "training-error": 0.16362048906511412,
262+
// "type": "add-preprocessing"
263+
// };
264+
265+
return (
266+
<div className="container p-4 mx-auto">
267+
<h1 className="text-2xl font-bold mb-4">Floating-Point Expression Optimization</h1>
268+
269+
<div className="bg-white rounded-lg p-4 shadow">
270+
<div id="history">
271+
<ol>
272+
{renderHistory(derivation, {
273+
fpCoreToTeX,
274+
formatAccuracy
275+
})}
276+
</ol>
277+
</div>
278+
</div>
279+
280+
<style>{`
281+
.math {
282+
overflow-x: auto;
283+
}
284+
.error {
285+
margin-left: 0.5rem;
286+
color: #4299e1;
287+
cursor: help;
288+
}
289+
.proof {
290+
margin: 0.5rem 0;
291+
}
292+
details summary {
293+
cursor: pointer;
294+
color: #4a5568;
295+
font-weight: 500;
296+
}
297+
.condition {
298+
font-style: italic;
299+
}
300+
`}</style>
301+
</div>
302+
);
303+
};
304+
305+
4306

5307
const DerivationComponent = ({ expressionId }: { expressionId: number }) => {
6308
const [derivations, setDerivations] = HerbieContext.useGlobal(HerbieContext.DerivationsContext)
@@ -30,11 +332,15 @@ const DerivationComponent = ({ expressionId }: { expressionId: number }) => {
30332
currentExpressionId = nextDerivation.origExpId
31333
}
32334

33-
return (
34-
<div>
35-
<Latex>{selectedDerivation.history}</Latex>
36-
</div>
37-
);
335+
return <div>
336+
selectedDerivation.derivation ?
337+
DerivationRenderer(selectedDerivation.derivation) :
338+
<Latex>
339+
{
340+
selectedDerivation.history
341+
}
342+
</Latex>
343+
</div>
38344
};
39345

40346
export { DerivationComponent };

src/herbie/ExpressionTable.tsx

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,7 @@ function ExpressionTable() {
195195
]
196196
setExpressions(newExpressions);
197197
setDerivations([
198-
new Derivation("<p>User Input Expression</p>", nextId(expressions), undefined),
198+
new Derivation("<p>User Input Expression</p>", nextId(expressions), undefined, undefined),
199199
...derivations,
200200
]);
201201
setSelectedExprId(selectedId)
@@ -245,7 +245,8 @@ function ExpressionTable() {
245245
// get suggested expressions with Herbie and put them in the expressions table
246246
const suggested = await herbiejsJobs.suggestExpressions(fpcorejs.mathjsToFPCore(expression.text, spec.expression, fpcorejs.getVarnamesMathJS(spec.expression)), sample, serverUrl)
247247

248-
248+
// TODO: Fix name collision
249+
const derivationsObjects = suggested.derivations;
249250
const histories = suggested.histories;
250251
const alternatives = suggested.alternatives;
251252

@@ -286,7 +287,7 @@ function ExpressionTable() {
286287
// The following code assumes the HTMLHistory[] returend by Herbie
287288
// is mapped to the alternatives array 1:1
288289
const d = histories[i];
289-
const newDerivation = new Derivation(d, newId, expression.id);
290+
const newDerivation = new Derivation(d, newId, expression.id, derivationsObjects[i]);
290291
newDerivations.push(newDerivation);
291292
}
292293

0 commit comments

Comments
 (0)