lisp- "自動車：契約違反が予想される：ペア？:(）"アクセスコントロールモデル内のオブジェクトを破棄中

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))) 

ここにテストコードがあります。

(stepper red1 st1) 

私はこのエラーを得続ける：私はこのようなst1.I試験でオブジェクトの1つを破壊する場合

(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)))]))) 

は

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

"マトリックス" であります私がObjを含むリストを破壊したい行列。 "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)は（cond用語の結果/代替が明示的beginを持っている）だけで(cdr matrix)と同じである(begin destroy-Obj Obj (cdr matrix))あるとき、私はまた、その結果に注目してください。おそらく、かっこが足りないので、実際には(destroy-Obj Obj (cdr matrix))という意味になります。