1

我最近开始使用 PLT-Redex，我想知道是否有人可以给我一些关于如何在 Racket 中实现 let* 表达式的指示。

现在我可以像这样写简单的 let 表达式

(let (x (+ 2 4)) in (* x 2))
(let (x (+ 2 4)) in (let (y (* x 2)) in y))

但是，如果我尝试如下复杂的 let 表达式（请参阅我的代码中的测试 4 和 5），我会得到多个输出值：

(let (x (+ 2 4)) in (let (y (* x 2)) in (* y y)))
(let (x (+ 2 4)) in (let (y (* x 2)) in (let (y (* x 2)) in (let (z (+ y 5)) in (+ (+ x y) z)))))

我想像这样重写上面的表达式

(let* ([x (+ 2 4)]
       [y (* x 2)]
       [z (+ y 5)]
    (+ (+ x y) z))

以下是我当前的 Redex 实施，以防有人想提供帮助。

在此先感谢温贝托

#lang racket
(require redex)

(define-language L
  (e ::=
     v
     x
     (let (x e) in e)
     (e ...)
     (aop e e))

  (v ::= number integer string boolean)
  (x  ::= variable-not-otherwise-mentioned)
  (aop ::= + - / *)

  (p (e ...))
  (P (e ... E e ...))
  
  (E ::= 
     hole
     (let (x E) in e)
     (aop E e))

);; 


(define-metafunction L
  [(subst (x_1 any_1 x_1)) any_1]
  [(subst (x_1 any_1 x_a)) x_a]

  [(subst (x any (let (x e_x) in e_body)))
   (let (x (subst (x any e_x))) in e_body)]

  [(subst (x any (let (x_a e_xa) in e_body)))
   (let (x_a  (subst (x any e_xa))) in (subst (x any e_body)))]

  [(subst (x any (aop e_1 e_2)))
   (aop (subst (x any e_1)) (subst (x any e_2)))]

  [(subst (x any v_2)) v_2]
);;

(define L-R
  (reduction-relation
   L            
   #:domain p
 
   (--> 
    (in-hole P (/ number_1 0))
    ,(error 'DivisionByZeroError)
    "error")
   
   (--> 
    (in-hole P (+ number_1 number_2))
    (in-hole P ,(+ (term number_1) (term number_2)))
    "add")
   
   (-->
    (in-hole P (* number_1 number_2))
    (in-hole P ,(* (term number_1) (term number_2)))
    "multiply")
   
   (-->
    (in-hole P (/ number_1 number_2))
    (in-hole P ,(/ (term number_1) (term number_2)))
    "divide")
   
   (--> 
    (in-hole P (- number_1 number_2))
    (in-hole P ,(- (term number_1) (term number_2)))
    "subtract")

    (-->
     (in-hole P (let (x_1 e_1) in e_2))
     (in-hole P (subst (x_1 e_1 e_2))) 
    "let")
));;;

(define (test-syntax)
  ;; Test 1
  (test-->> L-R
            (term  ((+ 2 3)))
            (term  (5)))
  
 ;; Test 2
  (test-->> L-R
            (term  ((let (x (+ 2 4)) in (* x 2))))
            (term  (12)))
  
  ;; Test 3
  (test-->> L-R
            (term  ((let (x (+ 2 4)) in (let (y (* x 2)) in y))))
            (term  (12)))
  
  ;; Test 4 ERROR
;  (test-->> L-R
;            (term  ((let (x (+ 2 4)) in (let (y (* x 2)) in (* y y)))))
;            (term  (144)))


  ;; Test 5 ERROR
;  (test-->> L-R
;            (term  ((let (x (+ 2 4)) in (let (y (* x 2)) in (let (y (* x 2)) in (let (z (+ y 5)) in (+ (+ x y) z)))))))
;            (term  (35)))


);;


(test-syntax)
(module+ test
  (test-results))
4

0 回答 0