lisp-"car: contract violation expected: pair? given: ()" while destroy an obj in an access control model

Question

Write a procedure to destroy an object in my access control model and simulate every situation. This is my code.

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

Here is the test code.

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

When I want to destroy one of the objects in st1.I test like this:

(stepper red1 st1)

I keep getting this error:

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

The "matrix" is the matrix which I want to destroy any list including "Obj". The "Obj" could be o1 or o2. I put the "M_1" into the Matrix. I want to put "m1" of "st1" into "M_1" "m1" has been defined. It should not be empty.So why this error happened? Thank you very much!!

Answer 1

From looking at the code you do (third (car matrix)) and in the recursive step (destroy-Obj Obj (cdr matrix)) implies matrix eventually will end up not being a pair. Thus your code needs to handle the event where matrix is not a pair or the the more specific () if that is the guaranteed alternative (i the event matrix always is a proper list).

I also notice the consequence when (eqv? o1 Obj) is (begin destroy-Obj Obj (cdr matrix)) which is the same as just (cdr matrix) (cond terms consequence/alternative has explicit begin). Perhaps you lack the parentheses so that you really meant (destroy-Obj Obj (cdr matrix)).