unbreak stlc-sub test #9

This commit is contained in:
Robby Findler 2014-03-18 17:02:36 -05:00
parent 9ca793a1c8
commit 9e41d393d5
2 changed files with 10 additions and 21 deletions

View File

@ -1,18 +1,8 @@
3,4d2
3c3
< (define the-error "no error")
<
7d4
< racket/match
8a6
> racket/match
12a11,12
---
> (define the-error "swaps to/from expressions when recurring in the rhs of app")
>
113a114,115
> [(subst (M N) x M_x)
> ((subst M_x x M) (subst N x M_x))]
118,119d119
< [(subst (M N) x M_x)
119c119
< ((subst M x M_x) (subst N x M_x))]
257a258
>
---
> ((subst M_x x M) (subst N x M_x))]

View File

@ -1,15 +1,15 @@
#lang racket/base
(define the-error "swaps to/from expressions when recurring in the rhs of app")
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "swaps to/from expressions when recurring in the rhs of app")
(define-language stlc
(M N ::=
@ -111,12 +111,12 @@
(λ (x τ) M)]
[(subst (λ (x_1 τ) M) x_2 v)
(λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
[(subst (M N) x M_x)
((subst M_x x M) (subst N x M_x))]
(where x_new ,(variable-not-in (term (x_1 e x_2))
(term x_1)))]
[(subst (c M) x M_x)
(c (subst M x M_x))]
[(subst (M N) x M_x)
((subst M_x x M) (subst N x M_x))]
[(subst M x M_x)
M])
@ -255,7 +255,6 @@
(generate-term stlc #:satisfying (typeof (tl nil) ((list int) (list int))) 5)]))
(match candidate
[`(typeof ,M ,τ)
M]
[#f #f]))