minikanren first practice

mk_model1.rkt

#lang racket

;There are 25 persons in three categories: A, B and C. Class a people always tell the truth, class B people always tell the lie, and class c people tell the truth and the lie separately (for example, if a class C person tells the truth this time, the next sentence he says must be the lie, and the next sentence is the truth again). The priest asked everyone, "are you a class?" 17 answered yes. The priest asked everyone, "are you a class B?" 12 answered yes. The priest asked everyone, "are you a class C?" Eight answered yes. Of these 25 people, how many class C person?

(require minikanren)

(define peano
  (lambda (n)
    (conde
      ((== 'z n))
      ((fresh (n-1)
         (== `(s ,n-1) n)
         (peano n-1))))))

(define addo
  (lambda (n1 n2 out)
    (conde
      ((== 'z n1)
       (== n2 out))
      ((fresh (n1-1 res)
         (== `(s ,n1-1) n1)
         (== `(s ,res) out)
         (addo n1-1 n2 res))))))

(define add3o
  (lambda (n1 n2 n3 out)
    (fresh (n12)
           (addo n12 n3 out)
           (addo n1 n2 n12))))

(define (asPeano x)
  (cond
    ((= x 0) 'z)
    (else `(s ,(asPeano (sub1 x))))))

(define (numPeano x)
  (cond
    ((eq? x 'z) 0)
    (else (add1 (numPeano (cadr x))))))

(define (asko role isRole lyingNumber otherNumber anwserNumber)
  (conde
   ((== role isRole) (== otherNumber anwserNumber))
   ((=/= role isRole) (== lyingNumber anwserNumber)))) 


(define (problem nA nB nC)
  (fresh (lC oC)
         (add3o nA nB nC (asPeano 25))
         (addo lC oC nC)
         (fresh (aA aB aC)
                (add3o aA aB aC (asPeano 17))
                (asko 'A 'A 'z nA aA)
                (asko 'B 'A nB 'z aB)
                (asko 'C 'A lC oC aC)
                )
         (fresh (aA aB aC)
                (add3o aA aB aC (asPeano 12))
                (asko 'A 'C 'z nA aA)
                (asko 'B 'C nB 'z aB)
                (asko 'C 'C oC lC aC)
                )
         (fresh (aA aB aC)
                (add3o aA aB aC (asPeano 8))
                (asko 'A 'B 'z nA aA)
                (asko 'B 'B nB 'z aB)
                (asko 'C 'B lC oC aC)
                )))