# [racket] [plt-scheme] [redex] matching question

On Fri, Jun 4, 2010 at 1:48 PM, Casey Klein
<clklein at eecs.northwestern.edu> wrote:
>* On Fri, Jun 4, 2010 at 1:14 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
*>>* Hi,
*>>*
*>>* I have a subtype? metafunction where one clause is as follows:
*>>*
*>>* ((subtype? C_0 C_1 CT)
*>>* #t
*>>* (side-condition (not (equal? (term C_0) (term Object))))
*>>* (where (C_0 C_2 any_1 any_2) (class-lookup C_0 CT))
*>>* (side-condition (not (equal? (term C_0) (term C_1))))
*>>* (side-condition (equal? (term C_2) (term C_1))))
*>>*
*>>* ie. C_0 is subtype of C_1 if C_0 directly inherits from C_1
*>>*
*>>* I find it redundant that I have to write the above, ie. introducing C_2 in the where clause to then check that C_2 and C_1 are equal.
*>>*
*>>* At first I wrote:
*>>*
*>>* ((subtype? C_0 C_1 CT)
*>>* #t
*>>* (side-condition (not (equal? (term C_0) (term Object))))
*>>* (where (C_0 C_1 any_1 any_2) (class-lookup C_0 CT))
*>>* (side-condition (not (equal? (term C_0) (term C_1)))))
*>>*
*>>* putting C_1 directly in the pattern of the where clause, but it did not work (that is to say, it always matched, even if the superclass was different from C_1).
*>>*
*>>* Can someone explain me why this is so?
*>>*
*>*
*>* John requested the same behavior a few months ago, and I agree it
*>* would be very handy. I'll try to implement it in the next few weeks.
*>*
*
This change is in git now. Here's an example.
(define-metafunction STLC
[(⊢ (e_1 e_2) Γ)
τ_2
(where (τ_1 → τ_2) (⊢ e_1 Γ))
(where τ_1 (⊢ e_2 Γ))]
[(⊢ x_i ((x_0 τ_0) ... (x_i τ_i) (x_i+1 τ_i+1) ...))
τ_i]
[(⊢ (λ (x : τ) e) ((x_0 τ_0) ...))
(τ → τ_*)
(where τ_* (⊢ e ((x τ) (x_0 τ_0) ...)))]
[(⊢ number Γ) Number]
[(⊢ e Γ) no-type])
(define-language STLC
(e (λ (x : τ) e)
(e e)
x
number)
(τ Number
(τ → τ))
(x variable-not-otherwise-mentioned)
(Γ ((x τ) ...)))