[plt-scheme] PLT Redex w/ 301.13

By the way, you need to run the example under the '(module ...)' language.

> -----Original Message-----
> From: plt-scheme-bounces at list.cs.brown.edu [mailto:plt-scheme-
> bounces at list.cs.brown.edu] On Behalf Of Williams, M. Douglas
> Sent: Wednesday, May 31, 2006 2:30 PM
> To: Paul A. Steckler
> Cc: plt-scheme at list.cs.brown.edu
> Subject: RE: [plt-scheme] PLT Redex w/ 301.13
> 
> As others have pointed out, the problem is you need to do something like
> 
> (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2 2)))
> 
> to require the reduction-semantics module.  And so on for others modules.
> 
> For example, to use an example from redex itself:
> 
> (module subject-reduction mzscheme
>   (require (planet "reduction-semantics.ss" ("robby" "redex.plt")))
>   (require (planet "gui.ss" ("robby" "redex.plt")))
>   (require (planet "subst.ss" ("robby" "redex.plt")))
>   (require (lib "plt-match.ss"))
> 
>   (reduction-steps-cutoff 10)
> 
>   (define lang
>     (language (e (e e)
>                  (abort e)
>                  x
>                  v)
>               (x (variable-except lambda call/cc abort))
>               (c (v c)
>                  (c e)
>                  hole)
>               (v call/cc
>                  number
>                  (lambda (x t) e))
>               (t num
>                  (t -> t))))
> 
>   (define reductions
>     (list
>      (reduction lang
>                 (in-hole c_1 (call/cc v_arg))
>                 (let ([v (variable-not-in (term c_1) 'x)])
>                   (plug
>                    (term c_1)
>                    (term (v_arg (lambda (,v)
>                                   (abort ,(plug (term c_1) v))))))))
>      (reduction lang
>                 (in-hole c (abort e_1))
>                 (term e_1))
>      (reduction/context lang
>                         c
>                         ((lambda (x_format t_1) e_body) v_actual)
>                         ;(lc-subst x_format v_actual e_body)
>                         (lc-subst (term x_format) (term e_body) (term
> v_actual))
>                         )))
> 
>   (define lc-subst
>     (plt-subst
>      [(? symbol?) (variable)]
>      [(? number?) (constant)]
>      [`(lambda (,x ,t) ,b)
>       (all-vars (list x))
>       (build (lambda (vars body) `(lambda (,(car vars) ,t) ,body)))
>       (subterm (list x) b)]
>      [`(call/cc ,v)
>       (all-vars '())
>       (build (lambda (vars arg) `(call/cc ,arg)))
>       (subterm '() v)]
>      [`(,f ,x)
>       (all-vars '())
>       (build (lambda (vars f x) `(,f ,x)))
>       (subterm '() f)
>       (subterm '() x)]))
> 
>   (define (type-check term)
>     (let/ec k
>       (let loop ([term term]
>                  [env '()])
>         (match term
>           [(? symbol?)
>             (let ([l (assoc term env)])
>               (if l
>                   (cdr l)
>                   (k #f)))]
>           [(? number?) 'num]
>           [`(lambda (,x ,t) ,b)
>             (let ([body (loop b (cons (cons x t) env))])
>               `(,t -> ,body))]
>           [`(,e1 ,e2)
>             (let ([t1 (loop e1 env)]
>                   [t2 (loop e2 env)])
>               (match t1
>                 [`(,td -> ,tr)
>                   (if (equal? td t2)
>                       tr
>                       (k #f))]
>                 [else (k #f)]))]))))
> 
>   (define (pred term1)
>     (let ([t1 (type-check term1)])
>       (lambda (term2)
>         (and t1
>              (equal? (type-check term2) t1)))))
> 
>   (define (show term)
>     (traces/pred lang reductions (list term) (pred term)))
> 
>   ;(show '((lambda (x num) x) 1))
>   (show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda
> (x num) x))))
>   )
> 
> Doug
> 
> > -----Original Message-----
> > From: Paul A. Steckler [mailto:steck at stecksoft.com]
> > Sent: Wednesday, May 31, 2006 2:16 PM
> > To: Williams, M. Douglas
> > Cc: Paul A. Steckler; plt-scheme at list.cs.brown.edu
> > Subject: Re: [plt-scheme] PLT Redex w/ 301.13
> >
> > > Have you tried removing the PLaneT cache - /home/steck/.plt-
> > scheme/planet/
> > > in this case - and retrying it?
> >
> > No change -- except it takes a little longer to get the error message.
> >
> > -- Paul
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme