lisp-「汽車：合同違規期望：對？給定:(）」同時銷燬訪問控制模型中的obj

Question

編寫一個過程以銷燬我的訪問控制模型中的對象並模擬每種情況。 這是我的代碼。

(define st1 (term (st 3 2 (,s0 ,s1 ,s2) (,o0 ,o1) ,br ,m1))) 
(define m1 (term ((,s0 control ,s0) (,s1 (trans ,r1) ,o0) (,s2 ,r2 ,o1)))) 
(define r1 (term read)) 
(define r2 (term write)) 
(define br (term (,r1 ,r2))) 
(define-language GD 
[Sub (sub natural)] 
[PObj (obj natural)] 
[Obj Sub 
    PObj] 
[AR own 
    control] 
    [BR (variable-except own control)] 
    [TR (trans BR)] 
    [Right BR 
    AR 
    TR] 
    [Priv (Sub Right Obj)] 
    [S  (Root Sub ...)] 
    [O  (PObj ...)] 
    [R  (BR ...)] 
    [M  (Priv ...)] 
    [State (st natural natural S O R M)] 
    [Root (sub 0)] 
) 

(define s1 (term (sub 1))) 
(define s2 (term (sub 2))) 
    (define s0 (term (sub 0))) 

(define o0 (term (obj 0))) 
    (define o1 (term (obj 1))) 
(define o2 (term (obj 2))) 
(define o3 (term (obj 3))) 

這裏是測試代碼。

(define red1 
    (reduction-relation 
    GD 
    (--> (st natural_1 natural_2 
     S (PObj_0 ... PObj_2 PObj_4 ...) 
     R M_1) 
    (st natural_1 ,(- (term natural_2) 1) 
     S (PObj_0 ... PObj_4 ...) 
     R M_2) 
    (where (PObj_1 ... PObj_2 PObj_3 ...) (PObj_0 ... PObj_2 PObj_4 ...)) 
    (where M_2 ,(destroy-Obj (term (PObj_2)) (term M_1))) 
    (computed-name (term (destroy PObj_2)))) 
    ) 
) 

(define (destroy-Obj Obj matrix) 
    (let ([o1 (third (car matrix))]) 
(cond 
[(eqv? (first Obj) 'obj) 
(cond 
    [(eqv? o1 Obj) destroy-Obj Obj (cdr matrix)] 
    [else (cons (car matrix) (destroy-Obj Obj (cdr matrix)))])] 

[else (cons (car matrix) (destroy-Obj Obj (cdr matrix)))]))) 

當我要摧毀這樣在st1.I測試的對象之一：

(stepper red1 st1) 

我不斷收到此錯誤：

car: contract violation 
    expected: pair? 
    given:() 

「黑客帝國」 是矩陣，我想要銷燬包括「Obj」在內的任何列表。 「對象」可能是o1或o2。 我把「M_1」放入矩陣中。我想把「st1」的「m1」寫入「M_1」 「m1」已被定義。它不應該是空的。那麼爲什麼這個錯誤發生？ 非常感謝！

Answer 1

從看代碼(third (car matrix))和遞歸步驟(destroy-Obj Obj (cdr matrix))意味着matrix最終將不會成爲一對。因此，您的代碼需要處理的事件matrix不是一對或更具體的()如果這是有保證的替代（我的事件matrix總是一個正確的列表）。

我還注意到後果時(eqv? o1 Obj)是(begin destroy-Obj Obj (cdr matrix))這是一樣的只是(cdr matrix)（cond方面的後果/替代有明確的begin）。也許你缺少括號，因此你的意思是(destroy-Obj Obj (cdr matrix))。