Rename halt -> failed and halt? -> failed?.

vcanumalla · Feb 13, 2021 · 2fabc4b · 2fabc4b
1 parent d34c2ae
commit 2fabc4b
Show file tree

Hide file tree

Showing 14 changed files with 59 additions and 59 deletions.
diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -52,7 +52,7 @@
      term=? term->datum clear-terms! term-cache weak-term-cache
      union? union union-contents union-guards union-values
      union-filter in-union in-union* in-union-guards in-union-values
-     result? result-value result-state ans ans? halt halt?
+     result? result-value result-state ans ans? failed failed?
      ; adt/box.rkt
      @box @box-immutable @box? @unbox @set-box!
      ; adt/list.rkt : Pair Constructors and Selectors

diff --git a/rosette/base/core/bool.rkt b/rosette/base/core/bool.rkt
@@ -444,13 +444,13 @@
     [(_ val msg) (syntax/loc stx ($assume val msg raise-exn:fail:svm:assume:user))]))
 
 (define (halt-svm ex)
-  (define result (halt ex (current-vc)))
+  (define result (failed ex (current-vc)))
   ((current-reporter) 'exception result)
   result)
 
 (define (halt-err ex) ; Treat an exn:fail? error as an assertion failure.
   (define result
-    (halt (make-exn:fail:svm:assert:err (exn-message ex) (exn-continuation-marks ex))
+    (failed (make-exn:fail:svm:assert:err (exn-message ex) (exn-continuation-marks ex))
           (asserting (current-vc) #f)))
   ((current-reporter) 'exception result)
   result)
@@ -466,7 +466,7 @@
 ; with vc0 as the initial vc. 
 ;
 ; If the evaluation of the body terminates abnormally with an exn:fail? exception,
-; (with-vc vc0 body) outputs (halt v vc*) where v is an exn:fail:svm? exception
+; (with-vc vc0 body) outputs (failed v vc*) where v is an exn:fail:svm? exception
 ; that represents the cause of the abnormal termination, and vc* is the vc
 ; generated during the evaluation, with vc0 as the initial vc.
 (define-syntax (with-vc stx)

diff --git a/rosette/base/core/eval.rkt b/rosette/base/core/eval.rkt
@@ -16,7 +16,7 @@
 ; and vc* captures the verification condition generated during the
 ; evaluation, starting from the current vc.
 ;
-; If the thunk terminates abnormally, the result is (halt ex vc*),
+; If the thunk terminates abnormally, the result is (failed ex vc*),
 ; where ex is an exn:fail:svm? exception that represents the cause
 ; of the abnormal termination, and vc* captures the verification
 ; condition generated during the evaluation, starting from the current vc.

diff --git a/rosette/base/core/reflect.rkt b/rosette/base/core/reflect.rkt
@@ -10,7 +10,7 @@
          term->datum clear-terms! term-cache weak-term-cache
          union? union union-contents union-guards union-values
          union-filter in-union in-union* in-union-guards in-union-values
-         (struct-out ans) (struct-out halt) result? result-value result-state
+         (struct-out ans) (struct-out failed) result? result-value result-state
          symbolics)
 
 (define (term=? s0 s1)

diff --git a/rosette/base/core/result.rkt b/rosette/base/core/result.rkt
@@ -1,6 +1,6 @@
 #lang racket
 
-(provide (struct-out ans) (struct-out halt)
+(provide (struct-out ans) (struct-out failed)
          result? result-value result-state)
 
 ; Represents the result of symbolic evaluation,
@@ -14,4 +14,4 @@
 ; Represents the result of an evaluation that resulted in
 ; an exn:fail? exception being raised. In this case,
 ; the result-value field stores the exception that was raised.
-(struct halt result () #:transparent)
+(struct failed result () #:transparent)
diff --git a/rosette/guide/scribble/reflection/state-log.txt b/rosette/guide/scribble/reflection/state-log.txt
@@ -229,7 +229,7 @@
    (0
     (u
      .
-     "(halt\n (exn:fail:svm:merge \"[merge] failed\" #<continuation-mark-set>)\n (vc (! b) b))\n"))))
+     "(failed\n (exn:fail:svm:merge \"[merge] failed\" #<continuation-mark-set>)\n (vc (! b) b))\n"))))
  #""
  #"")
 ((vc)

diff --git a/rosette/guide/scribble/reflection/state-reflection.scrbl b/rosette/guide/scribble/reflection/state-reflection.scrbl
@@ -7,7 +7,7 @@
                     vc vc? vc-assumes vc-asserts
                     clear-vc! with-vc vc-true vc-true?
                     result? result-value result-state
-                    ans ans? halt halt? clear-terms! term-cache weak-term-cache)
+                    ans ans? failed failed? clear-terms! term-cache weak-term-cache)
            racket)
           scribble/core scribble/html-properties scribble/example racket/sandbox
           racket/runtime-path 
@@ -152,7 +152,7 @@ See @racket[vc] for details.
  then the result is @racket[ans?], and its
  @racket[result-value] contains the value computed by
  @racket[expr]. If @racket[expr] fails, the result is
- @racket[halt?], and its @racket[result-value] contains an
+ @racket[failed?], and its @racket[result-value] contains an
  @racket[exn:fail?] exception that represents the cause of
  the abnormal termination. In either case,
  @racket[result-state] holds the final verification condition
@@ -193,14 +193,14 @@ See @racket[vc] for details.
               @defproc[(result-value [v result?]) any/c]
               @defproc[(result-state [v result?]) any/c] 
               @defproc[(ans?  [v any/c]) boolean?]
-              @defproc[(halt? [v any/c]) boolean?])]{
+              @defproc[(failed? [v any/c]) boolean?])]{
 
  A @racket[result?] value represents the result of symbolic
  evaluation, which includes an output value,
  @racket[(result-value v)], and a part of the output state,
  @racket[(result-state v)]. Every result is either
  @racket[ans?], if the evaluation terminated normally, or
- @racket[halt?] otherwise.
+ @racket[failed?] otherwise.
 
  See also @racket[with-vc].
 

diff --git a/rosette/lib/roseunit.rkt b/rosette/lib/roseunit.rkt
@@ -52,7 +52,7 @@
 (define-syntax-rule (with-ans-or-fail expr)
   (match (with-vc expr)
     [(ans v _)    v]
-    [(halt ex _)  (raise ex)]))
+    [(failed ex _)  (raise ex)]))
 
 
 ; Makes sure that a test suite clears all Rosette state after it terminates.

diff --git a/rosette/lib/trace/tool.rkt b/rosette/lib/trace/tool.rkt
@@ -63,7 +63,7 @@
 
 (define reporter
   (match-lambda*
-    [(list 'exception (halt e s))
+    [(list 'exception (failed e s))
      (define assumes (vc-assumes s))
      (define asserts (vc-asserts s))
      (define skip?

diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt
@@ -415,12 +415,12 @@
     [(_ expr) (check-bv-exn #px"expected bitvectors of same length" expr)]
     [(_ p expr)
      (match (with-vc expr)
-       [(halt e _)
+       [(failed e _)
         (define rx p)
         (cond [(procedure? p) (check-pred p e)]
               [else (check-pred exn:fail? e)
                     (check-true (regexp-match? rx (exn-message e)))])]
-       [r (check-pred halt? r)])]))
+       [r (check-pred failed? r)])]))
 
 (define-tests (check-lifted-unary)
   (define-symbolic* n @integer?)

diff --git a/test/base/bvlib.rkt b/test/base/bvlib.rkt
@@ -34,10 +34,10 @@
     [(_ expr) (check-bv-exn #px"expected bitvectors of same length" expr)]
     [(_ rx expr)
      (match (with-vc expr)
-       [(halt e _)
+       [(failed e _)
         (check-pred exn:fail? e)
         (check-true (regexp-match? rx (exn-message e)))]
-       [r (check-pred halt? r)])]))
+       [r (check-pred failed? r)])]))
 
 (define (check-unary op1 op c)
   (check≡ (op1 x) (op x (bv c 4)))

diff --git a/test/base/eval-guarded.rkt b/test/base/eval-guarded.rkt
@@ -29,9 +29,9 @@
     (check-store st e-store)
     (check-true (vc-eqv? sp e-assumes e-asserts))))
 
-(define-syntax-rule (check-halt actual e-exn? e-assumes e-asserts)
+(define-syntax-rule (check-failed actual e-exn? e-assumes e-asserts)
   (begin
-    (match-define (halt ex sp) actual)
+    (match-define (failed ex sp) actual)
     (check-pred e-exn? ex) 
     (check-true (vc-eqv? sp e-assumes e-asserts))))
 
@@ -50,17 +50,17 @@
   (check-ans (eval-assuming g (lambda () (@set-box! x 5) (@assert a) (@assume b)))
              (void) `((,x 0 5)) (&& g (=> a b)) (=> g a))
   ;---------------------------;
-  (check-halt (eval-assuming #f (const 1))
+  (check-failed (eval-assuming #f (const 1))
               exn:fail:svm:assume:core? #f #t)
-  (check-halt (eval-assuming g (lambda () (@set-box! x 2) (@assume (! g))))
+  (check-failed (eval-assuming g (lambda () (@set-box! x 2) (@assume (! g))))
               exn:fail:svm:assume:user? #f #t)
-  (check-halt (eval-assuming g (lambda () (@set-box! x 4) ($assume (! g))))
+  (check-failed (eval-assuming g (lambda () (@set-box! x 4) ($assume (! g))))
               exn:fail:svm:assume:core? #f #t)
-  (check-halt (eval-assuming g (lambda () (@set-box! x 5) (@assert #f)))
+  (check-failed (eval-assuming g (lambda () (@set-box! x 5) (@assert #f)))
               exn:fail:svm:assert:user? g (! g))
-  (check-halt (eval-assuming g (lambda () (@set-box! x 6) ($assert #f)))
+  (check-failed (eval-assuming g (lambda () (@set-box! x 6) ($assert #f)))
               exn:fail:svm:assert:core? g (! g))
-  (check-halt (eval-assuming g (lambda () (@set-box! x 7) (1)))
+  (check-failed (eval-assuming g (lambda () (@set-box! x 7) (1)))
               exn:fail:svm:assert:err? g (! g))
   ;---------------------------;
   (check-equal? (@unbox x) 3)

diff --git a/test/base/real.rkt b/test/base/real.rkt
@@ -23,7 +23,7 @@
 
 (define-syntax-rule (check-cast (type val) (accepted? out))
     (match (with-vc (type-cast type val))
-      [(and r (or (ans v sp) (halt v sp)))
+      [(and r (or (ans v sp) (failed v sp)))
        (when (ans? r) (check-equal? v out))
        (check-equal? (vc-assumes sp) #t)
        (check-equal? (vc-asserts sp) accepted?)]))
@@ -85,14 +85,14 @@
   (syntax-rules ()
     [(_ expr)
      (match (with-vc expr)
-       [(halt e _) (check-pred exn:fail? e)]
-       [r (check-pred halt? r)])]
+       [(failed e _) (check-pred exn:fail? e)]
+       [r (check-pred failed? r)])]
     [(_ rx expr)
      (match (with-vc expr)
-       [(halt e _)
+       [(failed e _)
         (check-pred exn:fail? e)
         (check-true (regexp-match? rx (exn-message e)))]
-       [r (check-pred halt? r)])]))
+       [r (check-pred failed? r)])]))
 
 (define-syntax-rule (check-state actual expected-value expected-asserts)
   (let ([r (with-vc actual)])

diff --git a/test/base/vc.rkt b/test/base/vc.rkt
@@ -98,16 +98,16 @@
   (check-pred vc-true? (vc))
   (check-match (with-vc (@assume a)) (ans (? void?) (app vc->pair (cons (== a) #t))))
   (check-pred vc-true? (vc))
-  (check-match (with-vc (@assume #f)) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
-  (check-match (with-vc ($assume #f)) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (@assume #f)) (failed (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc ($assume #f)) (failed (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
   ;---------------------------;
   (check-match (with-vc (@assert 1)) (ans (? void?) (? vc-true?)))
   (check-pred vc-true? (vc))
   (check-match (with-vc (@assert a)) (ans (? void?) (app vc->pair (cons #t (== a)))))
   (check-pred vc-true? (vc))
-  (check-match (with-vc (@assert #f)) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc ($assert #f)) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc (1)) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f)))))
+  (check-match (with-vc (@assert #f)) (failed (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc ($assert #f)) (failed (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (1)) (failed (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f)))))
 
 (define (check-with-vc-1)
   (define-symbolic a b c d @boolean?)
@@ -117,29 +117,29 @@
   (check-match (with-vc (begin (@assume a) (@assert b))) (ans (? void?) (app vc->pair (cons (== a) (== (=> a b))))))
   (check-match (with-vc (begin (@assert a) (@assume b))) (ans (? void?) (app vc->pair (cons (== (=> a b)) (== a)))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (@assume (! a)))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
-  (check-match (with-vc (begin ($assume a) (@assume (! a)))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
-  (check-match (with-vc (begin (@assume (! a)) ($assume a))) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
-  (check-match (with-vc (begin ($assume (! a)) ($assume a))) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin (@assume a) (@assume (! a)))) (failed (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin ($assume a) (@assume (! a)))) (failed (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin (@assume (! a)) ($assume a))) (failed (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin ($assume (! a)) ($assume a))) (failed (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assert a) (@assert (! a)))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc (begin ($assert a) (@assert (! a)))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc (begin (@assert (! a)) ($assert a))) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc (begin ($assert (! a)) ($assert a))) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc (begin (@assert a) (1))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assert a) (@assert (! a)))) (failed (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin ($assert a) (@assert (! a)))) (failed (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assert (! a)) ($assert a))) (failed (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin ($assert (! a)) ($assert a))) (failed (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assert a) (1))) (failed (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (@assert #f))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons (== a) (== (! a))))))
-  (check-match (with-vc (begin (@assume a) ($assert #f))) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons (== a) (== (! a))))))
-  (check-match (with-vc (begin (@assume a) (1))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) (@assert #f))) (failed (? exn:fail:svm:assert:user?) (app vc->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) ($assert #f))) (failed (? exn:fail:svm:assert:core?) (app vc->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) (1))) (failed (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (! a))))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assert a) (@assume #f))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons (== (! a)) (== a)))))
-  (check-match (with-vc (begin (@assert a) ($assume #f))) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons (== (! a)) (== a)))))
+  (check-match (with-vc (begin (@assert a) (@assume #f))) (failed (? exn:fail:svm:assume:user?) (app vc->pair (cons (== (! a)) (== a)))))
+  (check-match (with-vc (begin (@assert a) ($assume #f))) (failed (? exn:fail:svm:assume:core?) (app vc->pair (cons (== (! a)) (== a)))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume #f) (@assert a))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
-  (check-match (with-vc (begin (@assert #f) (@assume a))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
-  (check-match (with-vc (begin (1) (@assume a))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assume #f) (@assert a))) (failed (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin (@assert #f) (@assume a))) (failed (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (1) (@assume a))) (failed (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (1) (@assert b))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) (1) (@assert b))) (failed (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (! a))))))
   ;---------------------------;
   (check-match (with-vc (begin (@assume a) (@assume b) (@assert c) (@assert d)))
                (ans (? void?) (app vc->pair (cons (== (&& a b)) (== (&& (=> (&& a b) c) (=> (&& a b) d)))))))
@@ -151,9 +151,9 @@
                (ans (? void?) (app vc->pair (cons (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d))) (== (&& a (=> (=> a b) c)))))))
   ;---------------------------;
   (check-match (with-vc (begin (@assume a) (@assert b) (@assume #f) (@assert d)))
-               (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons (== (&& a (=> (=> a b) #f))) (== (=> a b))))))
+               (failed (? exn:fail:svm:assume:user?) (app vc->pair (cons (== (&& a (=> (=> a b) #f))) (== (=> a b))))))
   (check-match (with-vc (begin (@assume a) (@assert b) (1) (@assert d)))
-               (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (&& (=> a b) (=> a #f)))))))
+               (failed (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (&& (=> a b) (=> a #f)))))))
   ;---------------------------;
   (@assume a)
   (@assert b)
@@ -180,15 +180,15 @@
   (merge-vc! (list #f) (list vc0))
   (check-pred vc-true? (vc))
   ;---------------------------;
-  (match-define (halt _ vc1) (with-vc (@assume #f)))
+  (match-define (failed _ vc1) (with-vc (@assume #f)))
   (merge-vc! (list #f) (list vc1))
   (check-pred vc-true? (vc))
   (merge-vc! (list c) (list vc1))
   (check-match (vc) (app vc->pair (cons (== (=> c #f)) #t)))
   (check-exn-svm exn:fail:svm:assume:core? #rx"contradiction" (thunk (merge-vc! (list #t) (list vc1))))
   (clear-vc!)
   ;---------------------------;
-  (match-define (halt _ vc2) (with-vc (@assert #f)))
+  (match-define (failed _ vc2) (with-vc (@assert #f)))
   (merge-vc! (list #f) (list vc2))
   (check-pred vc-true? (vc))
   (merge-vc! (list c) (list vc2))
-Original file line number
+Diff line change
@@ Expand Up / @@ -229,7 +229,7 @@ @@
        (0
         (u
          .
-         "(halt\n (exn:fail:svm:merge \"[merge] failed\" #<continuation-mark-set>)\n (vc (! b) b))\n"))))
+         "(failed\n (exn:fail:svm:merge \"[merge] failed\" #<continuation-mark-set>)\n (vc (! b) b))\n"))))
      #""
      #"")
     ((vc)
@@ Expand Down @@