Stepper does not step for check-satisfied

[shhyou]

I am not sure if it is just me or for everyone. When trying to step this program:

#lang htdp/isl+
(define (my-add x)
  (lambda (y)
    (+ x y)))
(check-satisfied (my-add 5) procedure?)

The stepper expands check-satisfied and steps through its implementation. Moreover, adding this test:

(check-satisfied (my-add 5)
                 (lambda (g)
                   (and (procedure? g)
                        (= (g 3) 8))))

raises the error

lookup-binding: variable not found in environment: p?

[shhyou]

(This is the case since at least v8.8.)

[shhyou]

For this test:

#lang htdp/isl+
(check-satisfied (* 2 2) even?)

The stepper from v8.15 first shows (... {(* 2 2)} ...) -> (... {4} ...) and then begins to walk through this.

(let ((with-handlers-predicate1
        exn:fail:contract:arity?)
       (with-handlers-handler2
        (lambda (exn)
          (let ((msg (exn-message exn)))
            (let ((msg1
                   (regexp-match
                    (pregexp
                     "(.*): arity mismatch")
                    msg)))
              (cond
               (msg1
                (let ((raised-name (cadr msg1)))
                  (if (equal?
                       "even?"
                       raised-name)
                    (error-check
                     (lambda (v) #false)
                     "even?"
                     SATISFIED-FMT
                     #true)
                    (raise exn))))))))))
   (let ((bpz
          (continuation-mark-set-first
           #false
           break-enabled-key)))
     (call-handled-body
      bpz
      (lambda (e)
        (select-handler/no-breaks
         e
         bpz
         (list
          (cons
           with-handlers-predicate1
           with-handlers-handler2))))
      (lambda () (even? 4)))))

For this test:

#lang htdp/isl+
(check-satisfied (+ 2 3) (lambda (n) (even? (sub1 n))))

The stepper from v8.15 raises the error lookup-binding: variable not found in environment: p?.

A fix probably needs to rewrite the expansion of check-satisfied and to add more stepper hints.

[rfindler]

It probably makes sense to lift out the generated code into helper functions, like this:

(define-syntax (check-satisfied stx)
  (syntax-case stx ()
    [(_ actual:exp expected-predicate:id)
     (identifier? #'expected-predicate:id)
     (let* ([prop1 (first-order->higher-order #'expected-predicate:id)]
            [name (symbol->string (syntax-e  #'expected-predicate:id))]
            [code #`(lambda (x) (check-satisfied/proc x #,name #,prop1))])
       (check-expect-maker stx 
                           #'do-check-satisfied 
                           #'actual:exp
                           (list code name)
                           'comes-from-check-satisfied))]
    [(_ actual:exp expected-predicate:exp)
     (let ([pred #`(check-satisfied/pred expected-predicate:exp)])
       (check-expect-maker stx 
                           #'do-check-satisfied
                           #'actual:exp
                           (list pred "unknown name")
                           'comes-from-check-satisfied))]
    [(_ actual:exp expected-predicate:exp) 
     (raise-syntax-error 'check-satisfied "expects named function in second position." stx)]
    [_ (raise-syntax-error 'check-satisfied (argcount-error-message/stx 2 stx) stx)]))

(define (check-satisfied/pred p?)
  (let ((name (object-name p?)))
    (unless (and (procedure? p?) (procedure-arity-includes? p? 1))
      (if name  ;; this produces the BSL/ISL name 
          (error-check (lambda (v) #f) name SATISFIED-FMT #t)
          (error-check (lambda (v) #f) p? SATISFIED-FMT #t))))
  p?)

(define (check-satisfied/proc x name prop)
  (with-handlers ([exn:fail:contract:arity?
                   (lambda (exn)
                     (let* ((msg (exn-message exn))
                            (msg1 (regexp-match #px"(.*): arity mismatch" msg)))
                       (cond
                         [msg1
                          (let ((raised-name (cadr msg1)))
                            (if (equal? name raised-name)
                                (error-check (lambda (v) #f) name SATISFIED-FMT #t)
                                (raise exn)))]
                         [else (raise exn)])))])
    (prop x)))

[jbclements]

Huh. Okay, well, I just did some exploration, and it looks like Matthias added check-satisfied in 2014, but it appears that I never added support for it in the stepper. I went looking, and I don't actually see any discussion of it in my email.

To be perfectly honest, check-satisfied actually raises some interesting questions, from a stepper standpoint. Specifically, suppose the value being tested is a closure, and the predicate runs the procedure?

#lang htdp/isl+

(define (returns-five-when-called-with-six? f)
  (equal? (f 6) 5))


(define (my-fun x)
  9)

(check-satisfied my-fun returns-five-when-called-with-six?)

... Actually, this is kind of an interesting puzzle. I'm going to start a separate email.