fix unexpected memoization + add example illustrating need for uninte…

…rpreted functions

scpcf/heap/examples.rkt

@@ -20,10 +20,14 @@
       (if0 (zero? n) 1
            (+ (/ 2 (- 13 n)) (f (/ 1 (- 7 n))))))))
 
-((• 1 (((nat -> nat) -> (nat -> nat)) -> nat))
+((• 6 (((nat -> nat) -> (nat -> nat)) -> nat))
  (λ ([f : (nat -> nat)])
    (λ ([x : nat]) (/ 10 (f x)))))
 
-((• 1 (((nat -> nat) -> nat) -> nat))
+((• 7 (((nat -> nat) -> nat) -> nat))
  (λ ([f : (nat -> nat)])
    (/ 10 (- 10 (* (f 5) (f 7))))))
+
+((• 8 (((nat -> nat) nat nat -> nat) -> nat))
+ (λ ([f : (nat -> nat)] [x : nat] [y : nat])
+   (/ 1 (- 10 (* (f x) (f y))))))

scpcf/heap/semantics.rkt

@@ -134,7 +134,7 @@
   #:contract (havoc/n L (T ...) V)
   #:mode     (havoc/n I I       O)
   [(where (T_x ... -> T_y) T)
-   (where M (havocᵢ ,(fresh!) L T f))
+   (where M ,(havocᵢ (term L) (term T) (term f)))
    (where (X_l ...)
           ,(variables-not-in (term M) (make-list (length (term (T_l ...))) 'l)))
    (where (X_r ...)
@@ -144,12 +144,12 @@
             (λ ([X_l : T_l] ... [f : T] [X_r : T_r] ...) M))])
 
 ;; Synthesize havoc-ing expression for type `T`
-(define-metafunction SCPCFΣ
-  ; The first argument is a hack around Redex's memoization
-  havocᵢ : _ L T M -> M
-  [(havocᵢ _ L nat M) M]
-  [(havocᵢ _ L (T_x ... -> T_y) M)
-   (havocᵢ ,(fresh!) L T_y (@ L M (• ,(fresh!) T_x) ...))])
+;; I make this a function to get around Redex's memoization
+(define (havocᵢ L T M)
+  (match T
+    ['nat M]
+    [`(,T_x ... -> ,T_y)
+     (havocᵢ L T_y (list* '@ L M (for/list ([T_xᵢ T_x]) (list '• (fresh!) T_xᵢ))))]))
 
 (define-metafunction SCPCFΣ
   eq : M -> M