Merge issues resolved

src/core/batch.rkt

@@ -227,7 +227,7 @@
              (if (hash-has-key? rename-dict spec)
                  (car (hash-ref rename-dict spec))
                  spec)]
-            [(list '$impl (app eggref prec) (app eggref spec)) (list 'impl prec (loop spec 'real))]
+            [(list '$hole (app eggref prec) (app eggref spec)) (hole prec (loop spec 'real))]
             [(list '$approx spec (app eggref impl))
              (define spec* (vector-ref id->spec spec))
              (unless spec*

src/core/egg-herbie.rkt

@@ -132,7 +132,7 @@
   (for ([node (in-vector (batch-nodes insert-batch))]
         [root? (in-vector root-mask)]
         [n (in-naturals)])
-    (define idx
+    (define node*
       (match node
         [(literal v prec) (list '$literal (insert-node! prec #f) (insert-node! v #f))]
         [(? number?) node]
@@ -148,9 +148,9 @@
                       (define spec* (normalize-spec (batch-ref insert-batch spec)))
                       (define type (representation-type (repr-of-node insert-batch impl ctx)))
                       (cons spec* type))) ; preserved spec and type for extraction
-         (insert-node! (list '$approx (remap spec) (remap impl)) root?)]
-        [(list op (app remap args) ...) (insert-node! (cons op args) root?)]))
-
+         (list '$approx (remap spec) (remap impl))]
+        [(list op (app remap args) ...) (cons op args)]))
+    (define idx (insert-node! node* root?))
     (vector-set! mappings n idx))
 
   (for/list ([root (in-vector (batch-roots insert-batch))])
@@ -443,13 +443,13 @@
              (define res (sequential-product children))
              (set-box! budget (- (unbox budget) (length res)))
              (map (curry apply approx) res)])]
-         [(list 'impl prec spec)
+         [(hole prec spec)
           (define spec* (loop spec))
           (cond
             [(equal? (list #f) spec*) (list #f)]
             [else
              (set-box! budget (- (unbox budget) (length spec*)))
-             (map (curry list 'impl prec) spec*)])]
+             (map (curry hole prec) spec*)])]
          [`(Explanation ,body ...) (expand-proof body budget)]
          [(? list?)
           (define children (map loop term))
@@ -459,7 +459,7 @@
              (define res (sequential-product children))
              (set-box! budget (- (unbox budget) (length res)))
              res])]
-         [_ (error "Unknown proof term ~a" term)])])))
+         [_ (error 'expand-proof "Unknown proof term" term)])])))
 
 ;; Remove the front term if it doesn't have any rewrites
 (define (remove-front-term proof)

src/core/programs.rkt

@@ -21,7 +21,7 @@
 
 ;; Programs are just lisp lists plus atoms
 
-(define expr? (or/c list? symbol? boolean? real? literal? approx?))
+(define expr? (or/c list? symbol? boolean? real? literal? approx? hole?))
 
 ;; Returns repr name
 ;; Fast version does not recurse into functions applications
@@ -164,6 +164,8 @@
     (match* (prog loc)
       [(_ (? null?)) (f prog)]
       [((or (? literal?) (? number?) (? symbol?)) _) (invalid! prog loc)]
+      [((hole prec spec) (cons 1 rest))
+       (hole prec (loop spec rest))]
       [((approx spec impl) (cons idx rest)) ; approx nodes
        (case idx
          [(1) (approx (loop spec rest) impl)]