; does a cover b
(define (case-covers? data-layouts a b)
(let ([a-binding? (and (eqv? (ast-type a) 'var) (not (constructor? data-layouts a)))])
- (if (eqv? ':binding b)
- a-binding?
- (if a-binding?
- #t
- (if (eqv? (ast-type b) 'var)
- (eqv? b a)
+ (cond
+ [(eqv? ':binding b) a-binding?]
+ [a-binding? #t]
+ ; a literal/singleton
+ [(eqv? (ast-type b) 'var) (eqv? b a)]
+ ; two different constructors
+ [(not (eqv? (car a) (car b))) #f]
+ ; two same constructors
+ [else
(all (map (lambda (p q)
(case-covers? data-layouts p q))
- (cdr a) (cdr b))))))))
+ (cdr a) (cdr b)))])))
(define (verify-cases data-layouts annotated-program)