add missing value production

also, use redex-check? instead of redex-check in 2 places

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff

@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "app rule the range of the function is matched to the argument")
-31a32
+32a33
 >      ((cons v) v)
-53c54
+54c55
 <    (typeof Γ M_2 σ)
 ---
 >    (typeof Γ M_2 σ_2)
-236d236
+237d237
 < 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff

@@ -2,5 +2,5 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the ((cons number) v) value has been omitted")
-31a32
+32a33
 >      ((cons v) v)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff

@@ -2,9 +2,9 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the order of the types in the function position of application has been swapped")
-31a32
+32a33
 >      ((cons v) v)
-52c53
+53c54
 <   [(typeof Γ M (σ → σ_2))
 ---
 >   [(typeof Γ M (σ_2 → σ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff

@@ -2,9 +2,9 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the type of cons is incorrect")
-31a32
+32a33
 >      ((cons v) v)
-62c63
+63c64
 <    (int → ((list int) → (list int)))]
 ---
 >    (int → ((list int) → int))]

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff

@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the tail reduction returns the wrong value")
-31a32
+32a33
 >      ((cons v) v)
-91c92
+92c93
 <         (in-hole E v_2)
 ---
 >         (in-hole E v_1)
-236d236
+237d237
 < 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff

@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "hd reduction acts on partially applied cons")
-31a32
+32a33
 >      ((cons v) v)
-87c88
+88c89
 <    (--> (in-hole E (hd ((cons v_1) v_2)))
 ---
 >    (--> (in-hole E (hd (cons v_1)))
-236d236
+237d237
 < 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff

@@ -2,12 +2,12 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "evaluation isn't allowed on the rhs of applications")
-31a32
+32a33
 >      ((cons v) v)
-34,35c35
+35,36c36
 <      (E M)
 <      (v E)))
 ---
 >      (E M)))
-236d235
+237d236
 < 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff

@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "lookup always returns int")
-31a32
+32a33
 >      ((cons v) v)
-75c76
+76c77
 <    σ]
 ---
 >    int]
-236d236
+237d237
 < 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff

@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "variables aren't required to match in lookup")
-31a32
+32a33
 >      ((cons v) v)
-74c75
+75c76
 <   [(lookup (x σ Γ) x)
 ---
 >   [(lookup (x σ Γ) x_2)
-236d236
+237d237
 < 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)))
@@ -123,8 +124,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt

@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt

@@ -29,6 +29,7 @@
   (v (λ (x τ) M)
      c
      (cons v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -123,8 +124,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
+(define v? (redex-match? stlc v))
-(define τ? (redex-match stlc τ))
+(define τ? (redex-match? stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))