Cleanup.

sorawee · Feb 19, 2021 · 8fabaa8 · 8fabaa8
1 parent f803299
commit 8fabaa8
Show file tree

Hide file tree

Showing 6 changed files with 46 additions and 52 deletions.
diff --git a/rosette/base/adt/list.rkt b/rosette/base/adt/list.rkt
@@ -510,29 +510,26 @@
            (merge** ys (insert* _ i v))]))))
 
 (splicing-local
-    [(define (replace xs i v)
-       (let-values ([(left right) (split-at xs i)])
-         (append left (cons v (cdr right)))))
-     (define (replace* xs i v)
-       (apply merge* (for/list ([(x idx) (in-indexed xs)])
-                     (cons (@= i idx) (replace xs idx v)))))]
-  (define (@replace xs i v)
-    (or (and (list? xs) (number? i) (replace xs i v))
-        (match* ((type-cast @list? xs 'replace) (type-cast @integer? i 'replace))
-          [((? list? xs) (? number? i)) (replace xs i v)]
+    [(define ($list-set xs i v)
+       (for/list ([(x idx) (in-indexed xs)])
+         (merge (@= i idx) v x)))]
+  (define (@list-set xs i v)
+    (or (and (list? xs) (number? i) (list-set xs i v))
+        (match* ((type-cast @list? xs 'list-set) (type-cast @integer? i 'list-set))
+          [((? list? xs) (? number? i)) (list-set xs i v)]
           [((? list? xs) i) 
-           (assert-bound [0 @<= i @< (length xs)] 'replace)
-           (replace* xs i v)]
+           (assert-bound [0 @<= i @< (length xs)] 'list-set)
+           ($list-set xs i v)]
           [((union ys) (? number? i))
-           (assert-bound [0 <= i] 'replace)
+           (assert-bound [0 <= i] 'list-set)
            (apply merge* (assert-some 
                         (for/list ([y ys] #:when (< i (length (cdr y))))
-                          (cons (car y) (replace (cdr y) i v)))
+                          (cons (car y) (list-set (cdr y) i v)))
                         #:unless (length ys)
-                        (index-too-large-error 'replace xs i)))]
+                        (index-too-large-error 'list-set xs i)))]
           [((union ys) i)
-           (assert-bound [0 @<= i @< (@length xs)] 'replace)
-           (merge** ys (replace* _ i v))]))))
+           (assert-bound [0 @<= i @< (@length xs)] 'list-set)
+           (merge** ys ($list-set _ i v))]))))
 
 
 #|

diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -77,9 +77,9 @@
      @take @drop @split-at @take-right @drop-right @split-at-right
      @add-between @append* @flatten @remove-duplicates 
      @filter-map @count @partition @append-map @filter-not @shuffle 
-     @argmin @argmax 
+     @argmin @argmax @list-set
      ; adt/list.rkt : Non-Standard Functions
-     @insert @replace
+     @insert 
      ; adt/vector.rkt : Basic Functions
      @vector? @vector @vector-immutable 
      @vector-length @vector-ref @vector-set! @vector->list @list->vector @vector->immutable-vector 

diff --git a/rosette/base/core/term.rkt b/rosette/base/core/term.rkt
@@ -5,29 +5,29 @@
          "type.rkt" "reporter.rkt")
 
 (provide
- terms terms-count terms-ref with-terms clear-terms! gc-terms! term-cache
+ terms terms-count terms-ref with-terms clear-terms! gc-terms!
  term? constant? expression? 
  (rename-out [a-term term] [an-expression expression] [a-constant constant] [term-ord term-id]) 
  term-type term<? sublist? @app
  define-operator operator? operator-unsafe
  (all-from-out "type.rkt"))
 
 #|-----------------------------------------------------------------------------------|#
-; Term cache stores terms for the purposes of partial cannonicalization.
+; The current-terms cache stores terms for the purposes of partial cannonicalization.
 ; That is, it ensures that no syntactically identical terms are created.
-; It also assigns unique IDs (creation timestamps) to terms.  These IDs
-; are never reused, and they are used to impose an ordering on the children
+; The current-index parameter is used to assign unique IDs (creation timestamps) to terms.
+; These IDs are never reused, and they are used to impose an ordering on the children
 ; of expressions with commutative operators.
 #|-----------------------------------------------------------------------------------|#
-(define term-cache (make-parameter (make-hash)))
-(define term-count (make-parameter 0))
+(define current-terms (make-parameter (make-hash)))
+(define current-index (make-parameter 0))
 
-; Clears the entire term-cache if invoked with #f (default), or 
+; Clears the entire term cache if invoked with #f (default), or 
 ; it clears all terms reachable from the given set of leaf terms.
 (define (clear-terms! [terms #f])
   (if (false? terms)
-      (hash-clear! (term-cache))
-      (let ([cache (term-cache)]
+      (hash-clear! (current-terms))
+      (let ([cache (current-terms)]
             [evicted (list->mutable-set terms)])
         (for ([t terms])
           (hash-remove! cache (term-val t)))
@@ -41,10 +41,10 @@
               (set-add! evicted t))
             (loop))))))
 
-; Sets the current term-cache to a garbage-collected (weak) hash.
-; The setting preserves all reachable terms from (term-cache).
+; Sets the current term cache to a garbage-collected (weak) hash.
+; The setting preserves all reachable terms from (current-terms).
 (define (gc-terms!)
-  (unless (hash-weak? (term-cache)) ; Already a weak hash.
+  (unless (hash-weak? (current-terms)) ; Already a weak hash.
     (define cache
       (impersonate-hash
        (make-weak-hash)
@@ -55,36 +55,36 @@
        (lambda (h k) k)
        (lambda (h k) k)
        hash-clear!))
-    (for ([(k v) (term-cache)])
+    (for ([(k v) (current-terms)])
       (hash-set! cache k v))
-    (term-cache cache)))
+    (current-terms cache)))
 
-; Returns the term in the given term cache that has the given contents. If
+; Returns the term from current-terms that has the given contents. If
 ; no such term exists, failure-result is returned, unless it is a procedure.
 ; If failure-result is a procedure, it is called and its result is returned instead.
 (define (terms-ref contents [failure-result (lambda () (error 'terms-ref "no term for ~a" contents))])
-  (hash-ref (term-cache) contents failure-result))
+  (hash-ref (current-terms) contents failure-result))
 
-; Returns a list of all terms in the current term cache, in an unspecified order.
+; Returns a list of all terms in the current-term scache, in an unspecified order.
 (define (terms)
-  (hash-values (term-cache)))
+  (hash-values (current-terms)))
 
-; Returns the size of the current term cache.
+; Returns the size of the current-terms cache.
 (define (terms-count)
-  (hash-count (term-cache)))
+  (hash-count (current-terms)))
 
 ; Evaluates expr with (terms) set to terms-expr, returns the result, and
 ; restores (terms) to its old value. If terms-expr is not given, it defaults to
 ; (terms), so (with-terms expr) is equivalent to (with-terms (terms) expr).
 (define-syntax (with-terms stx)
   (syntax-parse stx
     [(_ expr)
-     #'(parameterize ([term-cache (hash-copy (term-cache))])
+     #'(parameterize ([current-terms (hash-copy (current-terms))])
          expr)]
     [(_ terms-expr expr)
-     #'(parameterize ([term-cache (hash-copy-clear (term-cache))])
+     #'(parameterize ([current-terms (hash-copy-clear (current-terms))])
          (let ([ts terms-expr]
-               [cache (term-cache)])
+               [cache (current-terms)])
            (for ([t ts])
              (hash-set! cache (term-val t) t))
            expr))]))
@@ -122,12 +122,12 @@
 
 (define-syntax-rule (make-term term-constructor args type rest ...) 
   (let ([val args])
-    (or (hash-ref (term-cache) val #f)
-        (let* ([ord (term-count)]
+    (or (hash-ref (current-terms) val #f)
+        (let* ([ord (current-index)]
                [out (term-constructor val type ord rest ...)])
-          (term-count (add1 ord))
+          (current-index (add1 ord))
           ((current-reporter) 'new-term out)
-          (hash-set! (term-cache) val out)
+          (hash-set! (current-terms) val out)
           out))))
 
 (define (make-const id t) 

diff --git a/rosette/guide/scribble/datatypes/pairs.scrbl b/rosette/guide/scribble/datatypes/pairs.scrbl
@@ -18,7 +18,7 @@
 @(define list-filtering (select '(filter remove remq remv remove* remq* remv* sort)))
 @(define list-searching (select '(member memv memq memf findf assoc assv assq assf)))
 @(define more-pair-ops (select '(caar cadr cdar cddr caaar caadr cadar caddr cdaar cdadr cddar cdddr caaaar caaadr caadar caaddr cadaar cadadr caddar cadddr cdaaar cdaadr cdadar cdaddr cddaar cddadr cdddar cddddr)))
-@(define more-list-ops (select '(empty cons? empty? first rest second third fourth fifth sixth seventh eighth ninth tenth last last-pair make-list take drop split-at takef dropf splitf-at take-right drop-right split-at-right takef-right dropf-right splitf-at-right add-between append* flatten remove-duplicates filter-map count partition range append-map filter-not shuffle permutations in-permutations argmin argmax )))
+@(define more-list-ops (select '(empty cons? empty? first rest second third fourth fifth sixth seventh eighth ninth tenth last last-pair make-list take drop split-at takef dropf splitf-at take-right drop-right split-at-right takef-right dropf-right splitf-at-right add-between append* flatten remove-duplicates filter-map count partition range append-map filter-not shuffle permutations in-permutations argmin argmax list-set)))
 
 @title[#:tag "sec:pair"]{Pairs and Lists}
 

diff --git a/rosette/lib/synthax.rkt b/rosette/lib/synthax.rkt
@@ -296,4 +296,4 @@
 (define (print-forms sol)
   (for ([f (generate-forms sol)])
     (printf "~a:~a:~a\n" (syntax-source f) (syntax-line f) (syntax-column f))
-    (pretty-display (syntax->datum f))))
+    (pretty-print (syntax->datum f))))
diff --git a/rosette/query/core.rkt b/rosette/query/core.rkt
@@ -153,8 +153,6 @@
   (define φ   (append assumes asserts))
 
   (define ¬φ `(,@assumes ,(apply || (map ! asserts))))
-
-  (define trial 0)
 
   (define (guess sol)
     (solver-assert guesser (evaluate φ sol))
@@ -180,8 +178,7 @@
         (let ([cex (check candidate)])
           (cond 
             [(unsat? cex) candidate]
-            [else (set! trial (add1 trial))
-                  (loop (guess cex))]))])))
+            [else (loop (guess cex))]))])))