Merge branch 'main' into new-encoding

src/api/demo.rkt

@@ -242,9 +242,8 @@
   (define resp
     (with-handlers ([exn:fail? (λ (e) (hash 'error (exn->string e)))])
       (fn post-data)))
-  (if (hash-has-key? resp 'error)
-      (eprintf "Error handling request: ~a\n" (hash-ref resp 'error))
-      (eprintf "Success handling request\n"))
+  (when (hash-has-key? resp 'error)
+    (eprintf "Error handling request: ~a\n" (hash-ref resp 'error)))
   (if (hash-has-key? resp 'error)
       (response 500
                 #"Bad Request"

src/api/server.rkt

@@ -136,20 +136,30 @@
                     #:when (equal? (hash-ref result 'command) "improve"))
            (get-table-data-from-hash result (make-path job-id)))])))
 
+(define (get-json-converter command)
+  (match (herbie-command-command command)
+    ['alternatives make-alternatives-result]
+    ['cost make-cost-result]
+    ['errors make-error-result]
+    ['evaluate make-calculate-result]
+    ['exacts make-exacts-result]
+    ['explanations make-explanation-result]
+    ['improve make-improve-result]
+    ['local-error make-local-error-result]
+    ['sample make-sample-result]
+    [_ (error 'compute-result "unknown command ~a" command)]))
+
 (define (herbie-do-server-job command job-id)
   (define herbie-result (wrapper-run-herbie command job-id))
-  (match-define (job-result kind test status time _ _ _ backend) herbie-result)
-  (match kind
-    ['alternatives (make-alternatives-result herbie-result test job-id)]
-    ['evaluate (make-calculate-result herbie-result job-id)]
-    ['cost (make-cost-result herbie-result job-id)]
-    ['errors (make-error-result herbie-result job-id)]
-    ['exacts (make-exacts-result herbie-result job-id)]
-    ['improve (make-improve-result herbie-result test job-id)]
-    ['local-error (make-local-error-result herbie-result job-id)]
-    ['explanations (make-explanation-result herbie-result job-id)]
-    ['sample (make-sample-result herbie-result test job-id)]
-    [_ (error 'compute-result "unknown command ~a" kind)]))
+  (define basic-output ((get-json-converter command) herbie-result job-id))
+  ;; Add default fields that all commands have
+  (hash-set* basic-output
+             'command
+             (~a (herbie-command-command command))
+             'job
+             job-id
+             'path
+             (make-path job-id)))
 
 (define completed-work (make-hash))
 
@@ -179,11 +189,6 @@
 (define manager #f)
 (define manager-dead-event #f)
 
-(define (get-command herbie-result)
-  ; force symbol type to string.
-  ; This is a HACK to fix JSON parsing errors that may or may not still happen.
-  (~s (job-result-command herbie-result)))
-
 (define (compute-job-id job-info)
   (sha1 (open-input-string (~s job-info))))
 
@@ -363,76 +368,36 @@
   (place-channel-put manager (list 'finished manager worker-id job-id out-result)))
 
 (define (make-explanation-result herbie-result job-id)
-  (hasheq 'command
-          (get-command herbie-result)
-          'explanation
-          (job-result-backend herbie-result)
-          'job
-          job-id
-          'path
-          (make-path job-id)))
+  (hasheq 'explanation (job-result-backend herbie-result)))
 
 (define (make-local-error-result herbie-result job-id)
-  (hasheq 'command
-          (get-command herbie-result)
-          'tree
-          (job-result-backend herbie-result)
-          'job
-          job-id
-          'path
-          (make-path job-id)))
-
-(define (make-sample-result herbie-result test job-id)
+  (hasheq 'tree (job-result-backend herbie-result)))
+
+(define (make-sample-result herbie-result job-id)
+  (define test (job-result-test herbie-result))
   (define pctx (job-result-backend herbie-result))
   (define repr (context-repr (test-context test)))
-  (hasheq 'command
-          (get-command herbie-result)
-          'points
-          (pcontext->json pctx repr)
-          'job
-          job-id
-          'path
-          (make-path job-id)))
+  (hasheq 'points (pcontext->json pctx repr)))
 
 (define (make-calculate-result herbie-result job-id)
-  (hasheq 'command
-          (get-command herbie-result)
-          'points
-          (job-result-backend herbie-result)
-          'job
-          job-id
-          'path
-          (make-path job-id)))
+  (hasheq 'points (job-result-backend herbie-result)))
 
 (define (make-cost-result herbie-result job-id)
-  (hasheq 'command
-          (get-command herbie-result)
-          'cost
-          (job-result-backend herbie-result)
-          'job
-          job-id
-          'path
-          (make-path job-id)))
+  (hasheq 'cost (job-result-backend herbie-result)))
 
 (define (make-error-result herbie-result job-id)
   (define errs
     (for/list ([pt&err (job-result-backend herbie-result)])
       (define pt (first pt&err))
       (define err (second pt&err))
       (list pt (format-bits (ulps->bits err)))))
-  (hasheq 'command (get-command herbie-result) 'points errs 'job job-id 'path (make-path job-id)))
+  (hasheq 'points errs))
 
 (define (make-exacts-result herbie-result job-id)
-  (hasheq 'command
-          (get-command herbie-result)
-          'points
-          (job-result-backend herbie-result)
-          'job
-          job-id
-          'path
-          (make-path job-id)))
-
-(define (make-improve-result herbie-result test job-id)
+  (hasheq 'points (job-result-backend herbie-result)))
+
+(define (make-improve-result herbie-result job-id)
+  (define test (job-result-test herbie-result))
   (define ctx (context->json (test-context test)))
   (define backend (job-result-backend herbie-result))
   (define job-time (job-result-time herbie-result))
@@ -447,9 +412,7 @@
       ['timeout #f]
       ['failure (exception->datum backend)]))
 
-  (hasheq 'command
-          (get-command herbie-result)
-          'status
+  (hasheq 'status
           (job-result-status herbie-result)
           'test
           test
@@ -464,11 +427,7 @@
           'profile
           profile
           'backend
-          backend-hash
-          'job
-          job-id
-          'path
-          (make-path job-id)))
+          backend-hash))
 
 (define (backend-improve-result-hash-table backend repr test)
   (define pcontext (improve-result-pctxs backend))
@@ -529,8 +488,9 @@
 (define (repr->json repr)
   (hasheq 'name (representation-name repr) 'type (representation-type repr)))
 
-(define (make-alternatives-result herbie-result test job-id)
+(define (make-alternatives-result herbie-result job-id)
 
+  (define test (job-result-test herbie-result))
   (define vars (test-vars test))
   (define repr (test-output-repr test))
 
@@ -559,17 +519,11 @@
   (define derivations
     (for/list ([altn altns])
       (render-json altn processed-pcontext test-pcontext (test-context test))))
-  (hasheq 'command
-          (get-command herbie-result)
-          'alternatives
+  (hasheq 'alternatives
           fpcores
           'histories
           histories
           'derivations
           derivations
           'splitpoints
-          splitpoints
-          'job
-          job-id
-          'path
-          (make-path job-id)))
+          splitpoints))

src/core/derivations.rkt

@@ -1,84 +1,34 @@
 #lang racket
 
 (require "../utils/alternative.rkt"
-         "points.rkt"
          "programs.rkt"
-         "egg-herbie.rkt"
-         "../syntax/sugar.rkt"
-         "../syntax/syntax.rkt")
+         "egg-herbie.rkt")
 
 (provide add-derivations)
 
-(define (canonicalize-proof prog proof loc pcontext ctx)
+(define (canonicalize-proof prog proof loc)
   (and proof
        ;; Proofs are actually on subexpressions,
        ;; we need to construct the proof for the full expression
        (for/list ([step (in-list proof)])
          (location-do loc prog (const step)))))
 
-;; Computes a `equal?`-based hash table key for an alternative
-(define (altn->key altn)
-  (match altn
-    [(alt expr `(rr ,loc ,method ,_) prevs _) (list expr (list 'rr loc method) (map alt-expr prevs))]
-    [(alt expr `(simplify ,loc ,method ,_) prevs _)
-     (list expr (list 'simplify loc method) (map alt-expr prevs))]
-    [_ (error 'altn->key "unimplemented ~a" altn)]))
-
-;; Creates two tables:
-;;  - map from alternative to a pair (e, l ~> r) where `e` is an `egg-runner`
-;;      and `l ~> r` is the rewrite we want a proof for.
-;;  - map from egg query to list of proofs
-(define (make-proof-tables altns)
-  (define alt->query&rws (make-hash))
-  (define query->rws (make-hash))
-
-  (define (build! altn)
-    (match altn
-      ; recursive rewrite using egg (impl -> impl)
-      [(alt expr `(,(or 'rr 'simplify) ,loc ,(? egg-runner? runner) #f) `(,prev) _)
-       (define start-expr (location-get loc (alt-expr prev)))
-       (define end-expr (location-get loc expr))
-       (define rewrite (cons start-expr end-expr))
-       (hash-set! alt->query&rws (altn->key altn) (cons runner rewrite))
-       (hash-update! query->rws runner (lambda (rws) (set-add rws rewrite)) '())]
-
-      ; everything else
-      [_ (void)])
-
-    altn)
-
-  ; build the table
-  (for ([altn (in-list altns)])
-    (alt-for-each build! altn))
-  (values alt->query&rws query->rws))
-
-;; Runs proof extraction.
-;; Result is a map from egg query to rewrites.
-(define (compute-proofs query->rws)
-  (for/hash ([(runner rws) (in-hash query->rws)])
-    (define proofs (run-egg runner `(proofs . ,rws)))
-    (values runner (map cons rws proofs))))
-
-;; Lookups a proof based on an alternative
-(define ((lookup-proof alt->query&rws query->proofs) altn)
-  (match-define (cons runner rw) (hash-ref alt->query&rws (altn->key altn)))
-  (cdr (assoc rw (hash-ref query->proofs runner))))
-
 ;; Adds proof information to alternatives.
-(define (add-derivations-to altn pcontext ctx alt->proof)
+(define (add-derivations-to altn)
   (match altn
     ; recursive rewrite or simplify, both using egg
-    [(alt expr (list phase loc (? egg-runner? runner) #f) `(,prev) _)
-     #:when (or (equal? phase 'simplify) (equal? phase 'rr))
-     (define proof (canonicalize-proof (alt-expr altn) (alt->proof altn) loc pcontext ctx))
-     (alt expr `(rr ,loc ,runner ,proof) `(,prev) '())]
+    [(alt expr (list (or 'simplify 'rr) loc (? egg-runner? runner) #f) `(,prev) _)
+     (define start-expr (location-get loc (alt-expr prev)))
+     (define end-expr (location-get loc expr))
+     (define proof (first (run-egg runner `(proofs ,(cons start-expr end-expr)))))
+     (define proof* (canonicalize-proof (alt-expr altn) proof loc))
+     (alt expr `(rr ,loc ,runner ,proof*) `(,prev) '())]
 
     ; everything else
     [_ altn]))
 
-(define (add-derivations alts pcontext ctx)
-  (define-values (alt->query&rws query->rws) (make-proof-tables alts))
-  (define query->proofs (compute-proofs query->rws))
-  (define lookup-proc (lookup-proof alt->query&rws query->proofs))
+(define (add-derivations alts)
+  (define cache (make-hash))
   (for/list ([altn (in-list alts)])
-    (alt-map (curryr add-derivations-to pcontext ctx lookup-proc) altn)))
+    ;; We need to cache this because we'll see the same alt several times
+    (alt-map (lambda (altn) (hash-ref! cache altn (lambda () (add-derivations-to altn)))) altn)))

src/core/mainloop.rkt

@@ -378,7 +378,7 @@
   (cond
     [(flag-set? 'generate 'proofs)
      (timeline-event! 'derivations)
-     (add-derivations alts (*pcontext*) (*context*))]
+     (add-derivations alts)]
     [else alts]))
 
 (define (sort-alts alts)

src/reports/common.rkt

@@ -202,7 +202,7 @@
      (define fabs-impl (get-fpcore-impl 'fabs (repr->prop r) (list r)))
      (define e (list fabs-impl x))
      (define c (context (list x) r r))
-     (format "~a = ~a" x* (converter* e c))]
+     (list (format "~a = ~a" x* (converter* e c)))]
     [(list 'negabs x)
      ; TODO: why are x* and x-sign unused?
      (define x* (string->symbol (format "~a_m" x)))
@@ -220,7 +220,7 @@
      (define vs* (context-vars ctx*))
      ;; We added some sign-* variables to the front of the variable
      ;; list in `ctx*`, we only want the originals here
-     (format-sort-instruction (take-right vs* (length vs)) language)]))
+     (list (format-sort-instruction (take-right vs* (length vs)) language))]))
 
 (define (format-sort-instruction vs l)
   (match l
@@ -278,37 +278,31 @@
   (define out-prog* (fpcore-add-props out-prog (list ':precision output-prec)))
 
   (define versions
-    (reap
-     [sow]
-     (for ([(lang record) (in-dict languages)])
-       (match-define (list ext converter) record)
-       (when (and (fpcore? out-prog*) (or (equal? ext "fpcore") (supported-by-lang? out-prog* ext)))
-         (define name
-           (if identifier
-               (symbol->string identifier)
-               "code"))
-         (define out (converter out-prog* name))
-         (define prelude-lines
-           (string-join
-            (append-map (lambda (instruction)
-                          (let ([l (format-prelude-instruction instruction ctx ctx* lang converter)])
-                            (if (list? l)
-                                l
-                                (list l))))
-                        instructions)
-            (if (equal? lang "TeX") "\\\\\n" "\n")
-            #:after-last "\n"))
-         (sow (cons lang
-                    ((if (equal? lang "TeX")
-                         (curry format "\\begin{array}{l}\n~a\\\\\n~a\\end{array}\n")
-                         string-append)
-                     prelude-lines
-                     out)))))))
-
-  (define math-out
-    (if (dict-has-key? versions "TeX")
-        (let ([val (dict-ref versions "TeX")]) val)
-        ""))
+    (reap [sow]
+          (for ([(lang record) (in-dict languages)])
+            (match-define (list ext converter) record)
+            (when (and (fpcore? out-prog*)
+                       (or (equal? ext "fpcore") (supported-by-lang? out-prog* ext)))
+              (define name
+                (if identifier
+                    (symbol->string identifier)
+                    "code"))
+              (define out (converter out-prog* name))
+              (define prelude-lines
+                (string-join
+                 (append-map (lambda (instruction)
+                               (format-prelude-instruction instruction ctx ctx* lang converter))
+                             instructions)
+                 (if (equal? lang "TeX") "\\\\\n" "\n")
+                 #:after-last "\n"))
+              (sow (cons lang
+                         ((if (equal? lang "TeX")
+                              (curry format "\\begin{array}{l}\n~a\\\\\n~a\\end{array}\n")
+                              string-append)
+                          prelude-lines
+                          out)))))))
+
+  (define math-out (dict-ref versions "TeX" ""))
 
   (define dropdown
     `(select (option "Math")