Skip to content

Commit b3cb7cb

Browse files
pavpanchekhapavpanchekha
authored
Merge pull request #1306 from herbie-fp/history-from-json
History from JSON
2 parents 8a1ac87 + 0787acc commit b3cb7cb

File tree

9 files changed

+154
-186
lines changed

9 files changed

+154
-186
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ rival
1717
regraph
1818
egg-herbie/pkg
1919
odyssey
20+
generic-flonum
2021

2122
# Racket
2223
*.zo

‎src/api/server.rkt‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -434,13 +434,16 @@
434434
[analysis (if (hash? backend-hash)
435435
(hash-ref backend-hash 'end)
436436
'())])
437-
(define history (read (open-input-string (hash-ref analysis 'history))))
438-
(define block `(div ([id "history"]) (ol ,@history)))
437+
(define history (hash-ref analysis 'history))
438+
(define block `(div ([id "history"]) (ol ,@(render-history history ctx))))
439439
(call-with-output-string (curry write-xexpr block))))
440440

441441
(define derivations
442-
(for/list ([altn (in-list altns)])
443-
(render-json altn pcontext (test-context test) errcache)))
442+
(for/list ([altn (in-list altns)]
443+
[analysis (if (hash? backend-hash)
444+
(hash-ref backend-hash 'end)
445+
'())])
446+
(hash-ref analysis 'history)))
444447

445448
(hasheq 'test
446449
(~s test-fpcore)
@@ -478,7 +481,7 @@
478481
(match-define (alt-analysis alt test-errors) analysis)
479482
(define cost (alt-cost alt repr))
480483

481-
(define history (render-history alt pcontext (test-context test) errcache))
484+
(define history-json (render-json alt pcontext (test-context test) errcache))
482485

483486
(define vars (test-vars test))
484487
(define splitpoints
@@ -491,7 +494,7 @@
491494
(hasheq 'expr
492495
(~s (alt-expr alt))
493496
'history
494-
(~s history)
497+
history-json
495498
'errors
496499
test-errors
497500
'cost

‎src/core/sampling.rkt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@
183183
(when (> (hash-ref table2 'infinite 0.0) (* 0.2 total))
184184
(warn 'inf-points
185185
#:url "faq.html#inf-points"
186-
"~a of points produce a very large (infinite) output. You may want to add a precondition."
187-
(format-accuracy (- total (hash-ref table2 'infinite)) total #:unit "%")))
186+
"~a% of points produce a very large (infinite) output. You may want to add a precondition."
187+
(~r (/ (- total (hash-ref table2 'infinite)) total 0.01) #:precision '(= 1))))
188188
(timeline-push! 'bogosity (combine-tables table table2))
189189
results)

‎src/reports/common.rkt‎

Lines changed: 16 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,8 @@
2525
"../syntax/platform.rkt"
2626
"../syntax/syntax.rkt")
2727

28-
(provide render-menu
28+
(provide format-accuracy
29+
render-menu
2930
render-warnings
3031
render-large
3132
render-comparison
@@ -36,7 +37,7 @@
3637
format-percent
3738
write-html
3839
program->fpcore
39-
program->tex
40+
fpcore->tex
4041
fpcore->string
4142
js-tex-include
4243
doc-url
@@ -51,6 +52,16 @@
5152
expr->tex
5253
core->js)
5354

55+
(define (format-accuracy numerator repr #:sign [sign #f] #:unit [unit ""])
56+
(define denominator (representation-total-bits repr))
57+
(cond
58+
[(and numerator (positive? denominator))
59+
(define percent (~r (- 100 (* (/ numerator denominator) 100)) #:precision '(= 1)))
60+
(if (and (positive? numerator) sign)
61+
(format "+~a~a" percent unit)
62+
(format "~a~a" percent unit))]
63+
[else ""]))
64+
5465
(define (write-html xexpr out)
5566
(fprintf out "<!doctype html>\n")
5667
(write-xexpr xexpr out))
@@ -148,10 +159,9 @@
148159
("Wolfram" "wl" ,core->wls)
149160
("TeX" "tex" ,(λ (c i) (core->tex c)))))
150161

151-
(define (program->tex prog ctx #:loc [loc #f])
152-
(define prog* (program->fpcore prog ctx))
153-
(if (supported-by-lang? prog* "tex")
154-
(core->tex prog* #:loc (and loc (cons 2 loc)) #:color "blue")
162+
(define (fpcore->tex fpcore #:loc [loc #f])
163+
(if (supported-by-lang? fpcore "tex")
164+
(core->tex fpcore #:loc (and loc (cons 2 loc)) #:color "blue")
155165
"ERROR"))
156166

157167
(define (render-program expr ctx #:ident [identifier #f] #:pre [precondition '(TRUE)])

‎src/reports/history.rkt‎

Lines changed: 69 additions & 98 deletions
Original file line numberDiff line numberDiff line change
@@ -55,21 +55,8 @@
5555

5656
(define (altn-errors altn pcontext ctx errcache mask)
5757
(define repr (context-repr ctx))
58-
(define repr-bits (representation-total-bits repr))
5958
(define err (errors-score-masked (hash-ref errcache (alt-expr altn)) mask))
60-
(format-accuracy err repr-bits #:unit "%"))
61-
62-
(define (expr->fpcore expr ctx #:ident [ident #f])
63-
(list 'FPCore
64-
(context-vars ctx)
65-
(let loop ([expr expr])
66-
(match expr
67-
[(? symbol?) expr]
68-
[(? number?) expr]
69-
[(? literal?) (literal-value expr)]
70-
[(approx spec impl) (loop impl)]
71-
[(hole precision spec) (loop spec)]
72-
[(list op args ...) (cons op (map loop args))]))))
59+
(format-accuracy err repr #:unit "%"))
7360

7461
(define (mixed->fpcore expr ctx)
7562
(define expr*
@@ -123,65 +110,49 @@
123110
(make-list (pcontext-length pcontext) #f))
124111

125112
;; HTML renderer for derivations
126-
(define (render-history altn pcontext ctx errcache [mask (make-mask pcontext)])
127-
(match altn
128-
[(alt prog 'start (list) _)
129-
(define err (altn-errors altn pcontext ctx errcache mask))
113+
(define (render-history json ctx)
114+
(define err
115+
(match (hash-ref json 'error)
116+
[(? number? n) (format-accuracy n (context-repr ctx) #:unit "%")]
117+
[other other]))
118+
(define prog (read (open-input-string (hash-ref json 'program))))
119+
(match (hash-ref json 'type)
120+
["start"
130121
(list `(li (p "Initial program " (span ((class "error")) ,err))
131-
(div ((class "math")) "\\[" ,(program->tex prog ctx) "\\]")))]
122+
(div ((class "math")) "\\[" ,(fpcore->tex prog) "\\]")))]
132123

133-
[(alt prog 'add-preprocessing `(,prev) _)
134-
;; TODO message to user is? proof later
135-
`(,@(render-history prev pcontext ctx errcache mask) (li "Add Preprocessing"))]
136-
137-
[(alt _ `(regimes ,splitpoints) prevs _)
138-
(define intervals
139-
(for/list ([start-sp (cons (sp -1 -1 #f) splitpoints)]
140-
[end-sp splitpoints])
141-
(interval (sp-cidx end-sp) (sp-point start-sp) (sp-point end-sp) (sp-bexpr end-sp))))
142-
(define repr (context-repr ctx))
124+
["add-preprocessing" `(,@(render-history (hash-ref json 'prev) ctx) (li "Add Preprocessing"))]
143125

126+
["regimes"
127+
(define prevs (hash-ref json 'prevs))
144128
`((li ((class "event")) "Split input into " ,(~a (length prevs)) " regimes")
145129
(li ,@(apply append
146-
(for/list ([entry prevs]
147-
[idx (in-naturals)]
148-
[new-mask (regimes-pcontext-masks pcontext splitpoints prevs ctx)])
149-
(define mask* (map and-fn mask new-mask))
150-
(define entry-ivals
151-
(filter (λ (intrvl) (= (interval-alt-idx intrvl) idx)) intervals))
152-
(define condition
153-
(string-join (map (curryr interval->string repr) entry-ivals) " or "))
154-
`((h2 (code "if " (span ((class "condition")) ,condition)))
155-
(ol ,@(render-history entry pcontext ctx errcache mask*))))))
130+
(for/list ([entry (in-list prevs)]
131+
[condition (in-list (hash-ref json 'conditions))])
132+
`((h2 (code "if " (span ((class "condition")) ,(string-join condition " or "))))
133+
(ol ,@(render-history entry ctx))))))
156134
(li ((class "event")) "Recombined " ,(~a (length prevs)) " regimes into one program."))]
157135

158-
[(alt prog `(taylor ,loc ,pt ,var) `(,prev) _)
159-
(define core (mixed->fpcore prog ctx))
160-
`(,@(render-history prev pcontext ctx errcache mask)
161-
(li (p "Taylor expanded in " ,(~a var) " around " ,(~a pt))
162-
(div ((class "math"))
163-
"\\[\\leadsto "
164-
,(core->tex core #:loc (and loc (cons 2 loc)) #:color "blue")
165-
"\\]")))]
136+
["taylor"
137+
(define-values (prev pt var loc) (apply values (map (curry hash-ref json) '(prev pt var loc))))
138+
`(,@(render-history prev ctx)
139+
(li (p "Taylor expanded in " ,var " around " ,pt)
140+
(div ((class "math")) "\\[\\leadsto " ,(fpcore->tex prog #:loc loc) "\\]")))]
166141

167-
[(alt prog `(evaluate ,loc) `(,prev) _)
168-
(define core (mixed->fpcore prog ctx))
169-
(define err (altn-errors altn pcontext ctx errcache mask))
170-
`(,@(render-history prev pcontext ctx errcache mask)
142+
["evaluate"
143+
(define-values (prev loc) (apply values (map (curry hash-ref json) '(prev loc))))
144+
`(,@(render-history prev ctx)
171145
(li (p "Evaluated real constant" (span ((class "error")) ,err))
172-
(div ((class "math"))
173-
"\\[\\leadsto "
174-
,(core->tex core #:loc (and loc (cons 2 loc)) #:color "blue")
175-
"\\]")))]
146+
(div ((class "math")) "\\[\\leadsto " ,(fpcore->tex prog #:loc loc) "\\]")))]
176147

177-
[(alt prog `(rr ,loc ,input ,proof) `(,prev) _)
178-
(define err (altn-errors altn pcontext ctx errcache mask))
179-
`(,@(render-history prev pcontext ctx errcache mask)
180-
(li ,(if proof
181-
(render-proof proof pcontext ctx errcache mask)
182-
""))
148+
["rr"
149+
(define-values (prev loc proof) (apply values (map (curry hash-ref json) '(prev loc proof))))
150+
`(,@(render-history prev ctx)
151+
(li ,(if (eq? proof (json-null))
152+
""
153+
(render-proof proof ctx)))
183154
(li (p "Applied rewrites" (span ((class "error")) ,err))
184-
(div ((class "math")) "\\[\\leadsto " ,(program->tex prog ctx #:loc loc) "\\]")))]))
155+
(div ((class "math")) "\\[\\leadsto " ,(fpcore->tex prog #:loc loc) "\\]")))]))
185156

186157
(define (errors-score-masked errs mask)
187158
(if (ormap identity mask)
@@ -191,31 +162,29 @@
191162
err))
192163
(errors-score errs)))
193164

194-
(define (render-proof proof pcontext ctx errcache mask)
195-
`(div ((class "proof"))
196-
(details (summary "Step-by-step derivation")
197-
(ol ,@(for/list ([step proof])
198-
(define-values (dir rule loc expr) (splice-proof-step step))
199-
;; need to handle mixed real/float expressions
200-
(define-values (err prog)
201-
(cond
202-
[(impl-prog? expr) ; impl program?
203-
(define score (errors-score-masked (hash-ref errcache expr) mask))
204-
(define bits (representation-total-bits (context-repr ctx)))
205-
(values (format-accuracy score bits) (program->fpcore expr ctx))]
206-
[else (values "N/A" (mixed->fpcore expr ctx))]))
207-
; the proof
208-
(if (equal? dir 'Goal)
209-
""
210-
`(li ,(let ([dir (match dir
211-
['Rewrite<= "right to left"]
212-
['Rewrite=> "left to right"])])
213-
`(p (code ([title ,dir]) ,(~a rule))
214-
(span ((class "error")) ,err)))
215-
(div ((class "math"))
216-
"\\[\\leadsto "
217-
,(core->tex prog #:loc (and loc (cons 2 loc)) #:color "blue")
218-
"\\]"))))))))
165+
(define (render-proof proof-json ctx)
166+
`(div
167+
((class "proof"))
168+
(details
169+
(summary "Step-by-step derivation")
170+
(ol ,@
171+
(for/list ([step (in-list proof-json)])
172+
(define-values (direction err loc rule prog-str)
173+
(apply values (map (curry hash-ref step) '(direction error loc rule program))))
174+
(define dir
175+
(match direction
176+
["goal" "goal"]
177+
["rtl" "right to left"]
178+
["ltr" "left to right"]))
179+
(define prog (read (open-input-string prog-str)))
180+
(if (equal? dir "goal")
181+
""
182+
`(li (p (code ([title ,dir]) ,rule)
183+
(span ((class "error"))
184+
,(if (number? err)
185+
(format-accuracy err (context-repr ctx) #:unit "%")
186+
err)))
187+
(div ((class "math")) "\\[\\leadsto " ,(fpcore->tex prog #:loc loc) "\\]"))))))))
219188

220189
(define (render-json altn pcontext ctx errcache [mask (make-list (pcontext-length pcontext) #f)])
221190
(define repr (context-repr ctx))
@@ -226,16 +195,17 @@
226195

227196
(match altn
228197
[(alt prog 'start (list) _)
229-
`#hash((program . ,(fpcore->string (expr->fpcore prog ctx))) (type . "start") (error . ,err))]
198+
`#hash((program . ,(fpcore->string (program->fpcore prog ctx))) (type . "start") (error . ,err))]
230199

231200
[(alt prog `(regimes ,splitpoints) prevs _)
232201
(define intervals
233202
(for/list ([start-sp (cons (sp -1 -1 #f) splitpoints)]
234203
[end-sp splitpoints])
235204
(interval (sp-cidx end-sp) (sp-point start-sp) (sp-point end-sp) (sp-bexpr end-sp))))
236205

237-
`#hash((program . ,(fpcore->string (expr->fpcore prog ctx)))
206+
`#hash((program . ,(fpcore->string (program->fpcore prog ctx)))
238207
(type . "regimes")
208+
(error . ,err)
239209
(conditions . ,(for/list ([entry prevs]
240210
[idx (in-naturals)])
241211
(define entry-ivals
@@ -247,7 +217,7 @@
247217
(render-json entry pcontext ctx errcache mask*))))]
248218

249219
[(alt prog `(taylor ,loc ,pt ,var) `(,prev) _)
250-
`#hash((program . ,(fpcore->string (expr->fpcore prog ctx)))
220+
`#hash((program . ,(fpcore->string (program->fpcore prog ctx)))
251221
(type . "taylor")
252222
(prev . ,(render-json prev pcontext ctx errcache mask))
253223
(pt . ,(~a pt))
@@ -256,14 +226,14 @@
256226
(error . ,err))]
257227

258228
[(alt prog `(evaluate ,loc) `(,prev) _)
259-
`#hash((program . ,(fpcore->string (expr->fpcore prog ctx)))
229+
`#hash((program . ,(fpcore->string (program->fpcore prog ctx)))
260230
(type . "evaluate")
261231
(prev . ,(render-json prev pcontext ctx errcache mask))
262232
(loc . ,loc)
263233
(error . ,err))]
264234

265235
[(alt prog `(rr ,loc ,input ,proof) `(,prev) _)
266-
`#hash((program . ,(fpcore->string (expr->fpcore prog ctx)))
236+
`#hash((program . ,(fpcore->string (program->fpcore prog ctx)))
267237
(type . "rr")
268238
(prev . ,(render-json prev pcontext ctx errcache mask))
269239
(proof . ,(if proof
@@ -273,7 +243,7 @@
273243
(error . ,err))]
274244

275245
[(alt prog 'add-preprocessing `(,prev) preprocessing)
276-
`#hash((program . ,(fpcore->string (expr->fpcore prog ctx)))
246+
`#hash((program . ,(fpcore->string (program->fpcore prog ctx)))
277247
(type . "add-preprocessing")
278248
(prev . ,(render-json prev pcontext ctx errcache mask))
279249
(error . ,err)
@@ -282,13 +252,14 @@
282252
(define (render-proof-json proof pcontext ctx errcache mask)
283253
(for/list ([step proof])
284254
(define-values (dir rule loc expr) (splice-proof-step step))
285-
(define err
286-
(if (impl-prog? expr)
287-
(errors-score-masked (hash-ref errcache expr) mask)
288-
"N/A"))
255+
(define-values (err fpcore)
256+
(cond
257+
[(impl-prog? expr)
258+
(values (errors-score-masked (hash-ref errcache expr) mask) (program->fpcore expr ctx))]
259+
[else (values "N/A" (mixed->fpcore expr ctx))]))
289260

290261
`#hash((error . ,err)
291-
(program . ,(fpcore->string (expr->fpcore expr ctx)))
262+
(program . ,(fpcore->string fpcore))
292263
(direction . ,(match dir
293264
['Rewrite<= "rtl"]
294265
['Rewrite=> "ltr"]

0 commit comments

Comments
 (0)