editor

mips assembler and disassembler

;; auxilary
(define (appendo x y z)
  (conde
   ((== x '()) (== y z))
   ((fresh (head xtail ytail ztail)
      (== x `(,head . ,xtail))
      (== z `(,head . ,ztail))
      (appendo xtail y ztail)))))

(define (mapo f l fl)
  (conde
   ((== l '()) (== fl '()))
   ((fresh (l-car l-cdr
                  fl-car fl-cdr)
      (== l `(,l-car . ,l-cdr))
      (== fl `(,fl-car . ,fl-cdr))
      (f l-car fl-car)
      (mapo f l-cdr fl-cdr)))))

;; Converting numerals to binary (lists of bits)
;;
;; converting to binary also takes the number of bits
;; so that we can pad it up to that with zeros
;;
;; lsb/msb direction?
(define (number->binary-aux len n m)
  (cond
   ((odd? n)
    (number->binary-aux (- len 1) (quotient (- n 1) 2) (cons 1 m)))
   ((and (not (zero? n)) (even? n))
    (number->binary-aux (- len 1) (quotient n 2) (cons 0 m)))
   ((zero? n) (cons len m))))

(define (number->binary len)
  (lambda (n)
    (if (number? n)
	(let ((len_b (number->binary-aux len n '())))
          (let ((len (car len_b))
                (b (cdr len_b)))
            (if (>= len 0)
                (append (make-list len 0) b)
                #f)))
	#f)))

(define (binary->number* b)
  (if (null? b)
      0
      (+ (car b)
         (* 2 (binary->number* (cdr b))))))

(define (binary->number b)
  (binary->number* (reverse b)))

;; miniKanren goals for binary conversion

(define (bijectiono f g x y)
  (fresh ()
    (watch x (lambda (x) (== y (f x))))
    (watch y (lambda (y) (== (g y) x)))))

(define (binaryo digits n b)
  (bijectiono (number->binary digits)
              binary->number
              n b))

;; This file is a minikanren version of
;; https://www.student.cs.uwaterloo.ca/~isg/res/mips/opcodes

(define (register r-name r-binary) (binaryo 5 r-name r-binary))
(define (shift a-numeral a-binary) (binaryo 5 a-numeral a-binary))
(define (immediate/16 i-number i-binary) (binaryo 16 i-number i-binary))
(define (immediate/26 i-number i-binary) (binaryo 26 i-number i-binary))

(define (instruction inst word)
  ;; Each MIPS instruction is encoded in exactly one word (32 bits).
  ;; There are three encoding formats.
  (conde
   ((register-encoding inst word))
   ((immediate-encoding inst word))
   ((jump-encoding inst word))))

(define (register-encoding inst word)
  ;; This encoding is used for instructions which do not require any immediate data.
  ;; These instructions receive all their operands in registers.
  ;; Additionally, certain of the bit shift instructions use this encoding; their operands are two registers and a 5-bit shift amount.
  ;; ooooooss sssttttt dddddaaa aaffffff
  (fresh (s o $d $s $t a i label)
    (fresh (o1 o2 o3 o4 o5 o6
               s1 s2 s3 s4 s5
               t1 t2 t3 t4 t5
               d1 d2 d3 d4 d5
               a1 a2 a3 a4 a5
               f1 f2 f3 f4 f5 f6)
      (== word `((,o1 ,o2 ,o3 ,o4 ,o5 ,o6 ,s1 ,s2)
                 (,s3 ,s4 ,s5 ,t1 ,t2 ,t3 ,t4 ,t5)
                 (,d1 ,d2 ,d3 ,d4 ,d5 ,a1 ,a2 ,a3)
                 (,a4 ,a5 ,f1 ,f2 ,f3 ,f4 ,f5 ,f6)))
      ;;(binaryo 32 inst word)
      (instruction-syntax 'register s inst
                          o $d $s $t a i label)
      (== '(0 0 0 0 0 0) `(,o1 ,o2 ,o3 ,o4 ,o5 ,o6))
      (register $s `(,s1 ,s2 ,s3 ,s4 ,s5))
      (register $t `(,t1 ,t2 ,t3 ,t4 ,t5))
      (register $d `(,d1 ,d2 ,d3 ,d4 ,d5))
      (shift a `(,a1 ,a2 ,a3 ,a4 ,a5))
      (instruction/opcode-function/syntax o `(,f1 ,f2 ,f3 ,f4 ,f5 ,f6) s))))

(define (immediate-encoding inst word)
  ;; This encoding is used for instructions which require a 16-bit immediate operand.
  ;; These instructions typically receive one operand in a register, another as an immediate value coded into the instruction itself, and place their results in a register.
  ;; This encoding is also used for load, store, branch, and other instructions so the use of the fields is different in some cases.
  ;; ooooooss sssttttt iiiiiiii iiiiiiii
  (fresh (s o $d $s $t a i label)
    (fresh (o1 o2 o3 o4 o5 o6
               s1 s2 s3 s4 s5
               t1 t2 t3 t4 t5
               i1 i2 i3 i4 i5 i6 i7 i8
               i9 i10 i11 i12 i13 i14 i15 i16)
      (== word `((,o1  ,o2  ,o3  ,o4  ,o5  ,o6  ,s1  ,s2)
                 (,s3  ,s4  ,s5  ,t1  ,t2  ,t3  ,t4  ,t5)
                 (,i1  ,i2  ,i3  ,i4  ,i5  ,i6  ,i7  ,i8)
                 (,i9  ,i10 ,i11 ,i12 ,i13 ,i14 ,i15 ,i16)))
      ;;(binaryo 32 inst word)
      (instruction-syntax 'immediate s inst
                          o $d $s $t a i label)
      (instruction/opcode-function/syntax o `(,o1 ,o2 ,o3 ,o4 ,o5 ,o6) s)
      (register $s `(,s1 ,s2 ,s3 ,s4 ,s5))
      (register $t `(,t1 ,t2 ,t3 ,t4 ,t5))
      (immediate/16 i `(,i1 ,i2 ,i3 ,i4 ,i5 ,i6 ,i7 ,i8
                            ,i9 ,i10 ,i11 ,i12 ,i13 ,i14 ,i15 ,i16)))))

(define (jump-encoding inst word)
  ;; This encoding is used for jump instructions, which require a 26-bit immediate offset.
  ;; It is also used for the trap instruction.
  ;; ooooooii iiiiiiii iiiiiiii iiiiiiii
  (fresh (s o $d $s $t a i label)
    (fresh (o1 o2 o3 o4 o5 o6
               i1 i2 i3 i4 i5 i6 i7 i8
               i9 i10 i11 i12 i13 i14 i15 i16
               i17 i18 i19 i20 i21 i22 i23 i24
               i25 i26)
      (== word `((,o1  ,o2  ,o3  ,o4  ,o5  ,o6  ,i1  ,i2)
                 (,i3  ,i4  ,i5  ,i6  ,i7  ,i8  ,i9  ,i10)
                 (,i11 ,i12 ,i13 ,i14 ,i15 ,i16 ,i17 ,i18)
                 (,i19 ,i20 ,i21 ,i22 ,i23 ,i24 ,i25 ,i26)))
      ;;(binaryo 32 inst word)
      (instruction-syntax 'jump s inst
                          o $d $s $t a i label)
      (instruction/opcode-function/syntax o `(,o1 ,o2 ,o3 ,o4 ,o5 ,o6) s)
      (immediate/26 i `(,i1 ,i2 ,i3 ,i4 ,i5 ,i6 ,i7 ,i8
                            ,i9 ,i10 ,i11 ,i12 ,i13 ,i14 ,i15 ,i16
                            ,i17 ,i18 ,i19 ,i20 ,i21 ,i22 ,i23 ,i24
                            ,i25 ,i26)))))

(define (instruction-syntax e s t
                            o $d $s $t a i label)
  ;; This is a table of all the different types of instruction as they appear in the assembly listing.
  ;; Note that each syntax is associated with exactly one encoding which is used to encode all instructions which use that syntax.
  (conde
   ((== e 'register)
    (conde
     ((== s 'arith-log)   (== t `(,o ,$d ,$s ,$t)))
     ((== s 'div-mult)    (== t `(,o ,$s ,$t)))
     ((== s 'shift)       (== t `(,o ,$d ,$t ,a)))
     ((== s 'shift-v)     (== t `(,o ,$d ,$t ,$s)))
     ((== s 'jump-r)      (== t `(,o ,$s)))
     ((== s 'move-from)   (== t `(,o ,$d)))
     ((== s 'move-to)     (== t `(,o ,$s)))))
   ((== e 'immediate)
    (conde
     ((== s 'arith-log-i) (== t `(,o ,$t ,$s ,i)))
     ((== s 'load-i)      (== t `(,o ,$t ,i)))
     ((== s 'branch)      (== t `(,o ,$s ,$t ,label)))
     ((== s 'branch-z)    (== t `(,o ,$s ,label)))
     ((== s 'load-store)  (== t `(,o ,$t ,i (,$s))))))
   ((== e 'jump)
    (conde
     ((== s 'jump)        (== t `(,o ,label)))
     ((== s 'trap)        (== t `(,o ,i)))))))

(define (instruction/opcode-function/syntax o f s)
  ;; These tables list all of the available operations `o` in MIPS.
  ;; For each instruction, the 6-bit opcode or function `f` is shown.
  ;; The syntax column `s` indicates which syntax is used to write the instruction in assembly text files. Note that which syntax is used for an instruction also determines which encoding is to be used.
  (conde
   ((== o 'add)   (== f '(1 0 0 0 0 0)) (== s 'arith-log))
   ((== o 'addu)  (== f '(1 0 0 0 0 1)) (== s 'arith-log))
   ((== o 'addi)  (== f '(0 0 1 0 0 0)) (== s 'arith-log-i))
   ((== o 'addiu) (== f '(0 0 1 0 0 1)) (== s 'arith-log-i))
   ((== o 'and)   (== f '(1 0 0 1 0 0)) (== s 'arith-log-i))
   ((== o 'andi)  (== f '(0 0 1 1 0 0)) (== s 'arith-log-i))
   ((== o 'div)   (== f '(0 1 1 0 1 0)) (== s 'div-mult))
   ((== o 'divu)  (== f '(0 1 1 0 1 1)) (== s 'div-mult))
   ((== o 'mult)  (== f '(0 1 1 0 0 0)) (== s 'div-mult))
   ((== o 'multu) (== f '(0 1 1 0 0 1)) (== s 'div-mult))
   ((== o 'nor)   (== f '(1 0 0 1 1 1)) (== s 'arith-log))
   ((== o 'or)    (== f '(1 0 0 1 0 1)) (== s 'arith-log))
   ((== o 'ori)   (== f '(0 0 1 1 0 1)) (== s 'arith-log-i))
   ((== o 'sll)   (== f '(0 0 0 0 0 0)) (== s 'shift))
   ((== o 'sllv)  (== f '(0 0 0 1 0 0)) (== s 'shift-v))
   ((== o 'sra)   (== f '(0 0 0 0 1 1)) (== s 'shift))
   ((== o 'srav)  (== f '(0 0 0 1 1 1)) (== s 'shift-v))
   ((== o 'srl)   (== f '(0 0 0 0 1 0)) (== s 'shift))
   ((== o 'srlv)  (== f '(0 0 0 1 1 0)) (== s 'shift-v))
   ((== o 'sub)   (== f '(1 0 0 0 1 0)) (== s 'arith-log))
   ((== o 'subu)  (== f '(1 0 0 0 1 1)) (== s 'arith-log))
   ((== o 'xor)   (== f '(1 0 0 1 1 0)) (== s 'arith-log))
   ((== o 'xori)  (== f '(0 0 1 1 1 0)) (== s 'arith-log-i))
   ((== o 'lhi)   (== f '(0 1 1 0 0 1)) (== s 'load-i))
   ((== o 'llo)   (== f '(0 1 1 0 0 0)) (== s 'load-i))
   ((== o 'slt)   (== f '(1 0 1 0 1 0)) (== s 'arith-log))
   ((== o 'sltu)  (== f '(1 0 1 0 0 1)) (== s 'arith-log))
   ((== o 'slti)  (== f '(0 0 1 0 1 0)) (== s 'arith-log-i))
   ((== o 'sltiu) (== f '(0 0 1 0 0 1)) (== s 'arith-log-i))
   ((== o 'beq)   (== f '(0 0 0 1 0 0)) (== s 'branch))
   ((== o 'bgtz)  (== f '(0 0 0 1 1 1)) (== s 'branch-z))
   ((== o 'blez)  (== f '(0 0 0 1 1 0)) (== s 'branch-z))
   ((== o 'bne)   (== f '(0 0 0 1 0 1)) (== s 'branch))
   ((== o 'j)     (== f '(0 0 0 0 1 0)) (== s 'jump))
   ((== o 'jal)   (== f '(0 0 0 0 1 1)) (== s 'jump))
   ((== o 'jalr)  (== f '(0 0 1 0 0 1)) (== s 'jump-r))
   ((== o 'jr)    (== f '(0 0 1 0 0 0)) (== s 'jump-r))
   ((== o 'lb)    (== f '(1 0 0 0 0 0)) (== s 'load-store))
   ((== o 'lbu)   (== f '(1 0 0 1 0 0)) (== s 'load-store))
   ((== o 'lh)    (== f '(1 0 0 0 0 1)) (== s 'load-store))
   ((== o 'lhu)   (== f '(1 0 0 1 0 1)) (== s 'load-store))
   ((== o 'lw)    (== f '(1 0 0 0 1 1)) (== s 'load-store))
   ((== o 'sb)    (== f '(1 0 1 0 0 0)) (== s 'load-store))
   ((== o 'sh)    (== f '(1 0 1 0 0 1)) (== s 'load-store))
   ((== o 'sw)    (== f '(1 0 1 0 1 1)) (== s 'load-store))
   ((== o 'mfhi)  (== f '(0 1 0 0 0 0)) (== s 'move-from))
   ((== o 'mflo)  (== f '(0 1 0 0 1 0)) (== s 'move-from))
   ((== o 'mthi)  (== f '(0 1 0 0 0 1)) (== s 'move-to))
   ((== o 'mtlo)  (== f '(0 1 0 0 1 1)) (== s 'move-to))
   ((== o 'trap)  (== f '(0 1 1 0 1 0)) (== s 'trap))))

(define (bito b)
  (conde ((== b 0)) ((== b 1))))

(define (really-binaryo w)
  (fresh (a b c d e f g h)
    (== w `(,a ,b ,c ,d ,e ,f ,g ,h))
    (bito a) (bito b) (bito c) (bito d)
    (bito e) (bito f) (bito g) (bito h)))

(define (eighto w)
  (fresh (a b c d e f g h)
    (== w `(,a ,b ,c ,d ,e ,f ,g ,h))))

(define (inst/binary inst bin)
  ;; 23bdfff8
  (fresh (word a b c d cd bcd abcd)
    (== word `(,a ,b ,c ,d))
    (eighto a)
    (eighto b)
    (eighto c)
    (eighto d)
    (appendo c d cd)
    (appendo b cd bcd)
    (appendo a bcd abcd)
    (binaryo 32 bin abcd)
    (instruction inst word)
    (really-binaryo a)
    (really-binaryo b)
    (really-binaryo c)
    (really-binaryo d)
    ))

(define (assemble/disassemble program binary)
  (mapo inst/binary program binary))

(define ackermann '(#x23bdfff8 #xafb00004 #xafbf0000 #x14800002 #x20a20001 #x08100012 #x14a00004 #x2084ffff #x20050001 #x0c100000 #x08100012 #x00808020 #x20a5ffff #x0c100000 #x2204ffff #x00402820 #x0c100000 #x08100012 #x8fb00004 #x8fbf0000 #x23bd0008 #x03e00008))

(assemble/disassemble q ackermann)

relational interpreter

;; relational scheme interpreter

(define lookupo
  (lambda (x env out)
    (fresh (y val env^)
      (== `((,y . ,val) . ,env^) env)
      (symbolo x)
      (symbolo y)
      (conde
        ((== x y) (== val out))
        ((=/= x y) (lookupo x env^ out))))))

(define unboundo
  (lambda (x env)
    (fresh ()
      (symbolo x)
      (conde
        ((== '() env))
        ((fresh (y v env^)
           (== `((,y . ,v) . ,env^) env)
           (=/= x y)
           (unboundo x env^)))))))

(define eval-expo
  (lambda (expr env out)
    (fresh ()
      (conde
        ((symbolo expr) ;; variable
         (lookupo expr env out))
        ((== `(quote ,out) expr)
         (absento 'closure out)
         (unboundo 'quote env))
        ((fresh (x body) ;; abstraction
           (== `(lambda (,x) ,body) expr)
           (== `(closure ,x ,body ,env) out)
           (symbolo x)
           (unboundo 'lambda env)))
        ((fresh (expr*)
           (== `(list . ,expr*) expr)
           (unboundo 'list env)
           (eval-exp*o expr* env out)))
        ((fresh (e1 e2 val x body env^) ;; application
           (== `(,e1 ,e2) expr)
           (eval-expo e1 env `(closure ,x ,body ,env^))
           (eval-expo e2 env val)
           (eval-expo body `((,x . ,val) . ,env^) out)))
        ((fresh (e1 e2 v1 v2)
           (== `(cons ,e1 ,e2) expr)
           (== `(,v1 . ,v2) out)
           (unboundo 'cons env)
           (eval-expo e1 env v1)
           (eval-expo e2 env v2)))
        ((fresh (e v2)
           (== `(car ,e) expr)
           (unboundo 'car env)
           (eval-expo e env `(,out . ,v2))))
        ((fresh (e v1)
           (== `(cdr ,e) expr)
           (unboundo 'cdr env)
           (eval-expo e env `(,v1 . ,out))))
        ((fresh (e v)
           (== `(null? ,e) expr)
           (conde
             ((== '() v) (== #t out))
             ((=/= '() v) (== #f out)))
           (unboundo 'null? env)
           (eval-expo e env v)))
        ((fresh (t c a b)
           (== `(if ,t ,c ,a) expr)
           (unboundo 'if env)
           (eval-expo t env b)
           (conde
             ((== #f b) (eval-expo a env out))
             ((=/= #f b) (eval-expo c env out)))))))))

(define eval-exp*o
  (lambda (expr* env out)
    (conde
      ((== '() expr*) (== '() out))
      ((fresh (a d res-a res-d)
         (== (cons a d) expr*)
         (== (cons res-a res-d) out)
         (eval-expo a env res-a)
         (eval-exp*o d env res-d))))))

;; running append in reverse
(eval-expo `((((lambda (f)
                 ((lambda (x)
                    (f (x x)))
                  (lambda (x)
                    (lambda (y) ((f (x x)) y)))))
               (lambda (my-append)
                 (lambda (l)
                   (lambda (s)
                     (if (null? l)
                         s
                         (cons (car l) ((my-append (cdr l)) s)))))))
              (quote ,x))
             (quote ,y)) '() '(a b c d e))

minikanren meta-interpreter

type inference

(define (!-o gamma expr type)
  (conde
    ((symbolo expr)
     (lookupo gamma expr type))
    ((numbero expr)
     (== 'int type))       
    ((== #f expr)
     (== 'bool type))       
    ((== #t expr)
     (== 'bool type))
    ((fresh (x e T1 T2)
       (== `(lambda (,x) ,e) expr)
       (== `(,T1 -> ,T2) type)
       (symbolo x)
       (!-o `((,x : ,T1) . ,gamma) e T2)))
    ((fresh (f e e^ t-ignore)
       (== `(let ((,f ,e)) ,e^) expr)
       (symbolo f)
       (!-o `((,f poly ,e ,gamma) . ,gamma) e^ type)
       (!-o gamma e t-ignore)))
    ((fresh (e1 e2 T)
       (== `(,e1 ,e2) expr)
       (!-o gamma e1 `(,T -> ,type))
       (!-o gamma e2 T)))
    ((fresh (e1 e2)
       (== `(+ ,e1 ,e2) expr)
       (== 'int type)
       (!-o gamma e1 'int)
       (!-o gamma e2 'int)))
    ((fresh (e1 e2 T1 T2)
       (== `(cons ,e1 ,e2) expr)
       (== `(pair ,T1 ,T2) type)
       (!-o gamma e1 T1)
       (!-o gamma e2 T2)))       
    ((fresh (e1 e2 e3)
       (== `(if ,e1 ,e2 ,e3) expr)
       (!-o gamma e1 'bool)
       (!-o gamma e2 type)
       (!-o gamma e3 type)))))

(define (lookupo gamma x t)
  (fresh ()
    (symbolo x)
    (conde
      ((fresh (e gamma^ _)
         (== `((,x poly ,e ,gamma^) . ,_) gamma)
         (!-o gamma^ e t)))
      ((fresh (_)
         (== `((,x : ,t) . ,_) gamma)))                         
      ((fresh (y _ gamma^)
         (== `((,y . ,_) . ,gamma^) gamma)
         (=/= x y)
         (symbolo y)
         (lookupo gamma^ x t))))))

(!-o '() '(let ((f (lambda (x) x))) (f (cons (f 5) (f #t)))) q)

numbers

;; number relations based on "oleg numbers"

(define (appendo x y z)
 (conde
  ((== x '()) (== y z))
  ((fresh (head xtail ytail ztail)
    (== x `(,head . ,xtail))
    (== z `(,head . ,ztail))
    (appendo xtail y ztail)))))

(define zeroo
  (lambda (n)
    (== '() n)))

(define poso
  (lambda (n)
    (fresh (a d)
      (== `(,a . ,d) n))))

(define >1o
  (lambda (n)
    (fresh (a ad dd)
      (== `(,a ,ad . ,dd) n))))

(define full-addero
  (lambda (b x y r c)
    (conde
      ((== 0 b) (== 0 x) (== 0 y) (== 0 r) (== 0 c))
      ((== 1 b) (== 0 x) (== 0 y) (== 1 r) (== 0 c))
      ((== 0 b) (== 1 x) (== 0 y) (== 1 r) (== 0 c))
      ((== 1 b) (== 1 x) (== 0 y) (== 0 r) (== 1 c))
      ((== 0 b) (== 0 x) (== 1 y) (== 1 r) (== 0 c))
      ((== 1 b) (== 0 x) (== 1 y) (== 0 r) (== 1 c))
      ((== 0 b) (== 1 x) (== 1 y) (== 0 r) (== 1 c))
      ((== 1 b) (== 1 x) (== 1 y) (== 1 r) (== 1 c)))))

(define addero
  (lambda (d n m r)
    (conde
      ((== 0 d) (== '() m) (== n r))
      ((== 0 d) (== '() n) (== m r)
       (poso m))
      ((== 1 d) (== '() m)
       (addero 0 n '(1) r))
      ((== 1 d) (== '() n) (poso m)
       (addero 0 '(1) m r))
      ((== '(1) n) (== '(1) m)
       (fresh (a c)
         (== `(,a ,c) r)
         (full-addero d 1 1 a c)))
      ((== '(1) n) (gen-addero d n m r))
      ((== '(1) m) (>1o n) (>1o r)
       (addero d '(1) n r))
      ((>1o n) (gen-addero d n m r)))))

(define gen-addero
  (lambda (d n m r)
    (fresh (a b c e x y z)
      (== `(,a . ,x) n)
      (== `(,b . ,y) m) (poso y)
      (== `(,c . ,z) r) (poso z)
      (full-addero d a b c e)
      (addero e x y z))))

(define pluso
  (lambda (n m k)
    (addero 0 n m k)))

(define minuso
  (lambda (n m k)
    (pluso m k n)))

(define *o
  (lambda (n m p)
    (conde
      ((== '() n) (== '() p))
      ((poso n) (== '() m) (== '() p))
      ((== '(1) n) (poso m) (== m p))
      ((>1o n) (== '(1) m) (== n p))
      ((fresh (x z)
         (== `(0 . ,x) n) (poso x)
         (== `(0 . ,z) p) (poso z)
         (>1o m)
         (*o x m z)))
      ((fresh (x y)
         (== `(1 . ,x) n) (poso x)
         (== `(0 . ,y) m) (poso y)
         (*o m n p)))
      ((fresh (x y)
         (== `(1 . ,x) n) (poso x)
         (== `(1 . ,y) m) (poso y)
         (odd-*o x n m p))))))

(define odd-*o
  (lambda (x n m p)
    (fresh (q)
      (bound-*o q p n m)
      (*o x m q)
      (pluso `(0 . ,q) m p))))

(define bound-*o
  (lambda (q p n m)
    (conde
      ((== '() q) (poso p))
      ((fresh (a0 a1 a2 a3 x y z)
         (== `(,a0 . ,x) q)
         (== `(,a1 . ,y) p)
         (conde
           ((== '() n)
            (== `(,a2 . ,z) m)
            (bound-*o x y z '()))
           ((== `(,a3 . ,z) n) 
            (bound-*o x y z m))))))))

(define =lo
  (lambda (n m)
    (conde
      ((== '() n) (== '() m))
      ((== '(1) n) (== '(1) m))
      ((fresh (a x b y)
         (== `(,a . ,x) n) (poso x)
         (== `(,b . ,y) m) (poso y)
         (=lo x y))))))

(define <lo
  (lambda (n m)
    (conde
      ((== '() n) (poso m))
      ((== '(1) n) (>1o m))
      ((fresh (a x b y)
         (== `(,a . ,x) n) (poso x)
         (== `(,b . ,y) m) (poso y)
         (<lo x y))))))

(define <=lo
  (lambda (n m)
    (conde
      ((=lo n m))
      ((<lo n m)))))

(define <o
  (lambda (n m)
    (conde
      ((<lo n m))
      ((=lo n m)
       (fresh (x)
         (poso x)
         (pluso n x m))))))

(define <=o
  (lambda (n m)
    (conde
      ((== n m))
      ((<o n m)))))

(define /o
  (lambda (n m q r)
    (conde
      ((== r n) (== '() q) (<o n m))
      ((== '(1) q) (=lo n m) (pluso r m n)
       (<o r m))
      ((<lo m n)
       (<o r m)
       (poso q)
       (fresh (nh nl qh ql qlm qlmr rr rh)
         (splito n r nl nh)
         (splito q r ql qh)
         (conde
           ((== '() nh)
            (== '() qh)
            (minuso nl r qlm)
            (*o ql m qlm))
           ((poso nh)
            (*o ql m qlm)
            (pluso qlm r qlmr)
            (minuso qlmr nl rr)
            (splito rr r '() rh)
            (/o nh m qh rh))))))))

(define splito
  (lambda (n r l h)
    (conde
      ((== '() n) (== '() h) (== '() l))
      ((fresh (b n^)
         (== `(0 ,b . ,n^) n)
         (== '() r)
         (== `(,b . ,n^) h)
         (== '() l)))
      ((fresh (n^)
         (==  `(1 . ,n^) n)
         (== '() r)
         (== n^ h)
         (== '(1) l)))
      ((fresh (b n^ a r^)
         (== `(0 ,b . ,n^) n)
         (== `(,a . ,r^) r)
         (== '() l)
         (splito `(,b . ,n^) r^ '() h)))
      ((fresh (n^ a r^)
         (== `(1 . ,n^) n)
         (== `(,a . ,r^) r)
         (== '(1) l)
         (splito n^ r^ '() h)))
      ((fresh (b n^ a r^ l^)
         (== `(,b . ,n^) n)
         (== `(,a . ,r^) r)
         (== `(,b . ,l^) l)
         (poso l^)
         (splito n^ r^ l^ h))))))

(define logo
  (lambda (n b q r)
    (conde
      ((== '(1) n) (poso b) (== '() q) (== '() r))
      ((== '() q) (<o n b) (pluso r '(1) n))
      ((== '(1) q) (>1o b) (=lo n b) (pluso r b n))
      ((== '(1) b) (poso q) (pluso r '(1) n))
      ((== '() b) (poso q) (== r n))
      ((== '(0 1) b)
       (fresh (a ad dd)
         (poso dd)
         (== `(,a ,ad . ,dd) n)
         (exp2 n '() q)
         (fresh (s)
           (splito n dd r s))))
      ((fresh (a ad add ddd)
         (conde
           ((== '(1 1) b))
           ((== `(,a ,ad ,add . ,ddd) b))))
       (<lo b n)
       (fresh (bw1 bw nw nw1 ql1 ql s)
         (exp2 b '() bw1)
         (pluso bw1 '(1) bw)
         (<lo q n)
         (fresh (q1 bwq1)
           (pluso q '(1) q1)
           (*o bw q1 bwq1)
           (<o nw1 bwq1))
         (exp2 n '() nw1)
         (pluso nw1 '(1) nw)
         (/o nw bw ql1 s)
         (pluso ql '(1) ql1)
         (<=lo ql q)
         (fresh (bql qh s qdh qd)
           (repeated-mul b ql bql)
           (/o nw bw1 qh s)
           (pluso ql qdh qh)
           (pluso ql qd q)
           (<=o qd qdh)
           (fresh (bqd bq1 bq)
             (repeated-mul b qd bqd)
             (*o bql bqd bq)
             (*o b bq bq1)
             (pluso bq r n)
             (<o n bq1))))))))

(define exp2
   (lambda (n b q)
     (conde
       ((== '(1) n) (== '() q))
       ((>1o n) (== '(1) q)
        (fresh (s)
          (splito n b s '(1))))
       ((fresh (q1 b2)
          (== `(0 . ,q1) q)
          (poso q1)
          (<lo b n)
          (appendo b `(1 . ,b) b2)
          (exp2 n b2 q1)))
       ((fresh (q1 nh b2 s)
          (== `(1 . ,q1) q)
          (poso q1)
          (poso nh)
          (splito n b s nh)
          (appendo b `(1 . ,b) b2)
          (exp2 nh b2 q1))))))

(define repeated-mul
  (lambda (n q nq)
    (conde
      ((poso n) (== '() q) (== '(1) nq))
      ((== '(1) q) (== n nq))
      ((>1o q)
       (fresh (q1 nq1)
         (pluso q1 '(1) q)
         (repeated-mul n q1 nq1)
         (*o nq1 n nq))))))

(define expo
  (lambda (b q n)
    (logo n b q '())))

;; factor the number 420 by running multiplication backwards!
(*o x y '(0 0 1 0 0 1 0 1 1))

reasoned schemer prelude

(define caro
  (lambda (p a)
    (fresh (d)
      (== (cons a d) p))))

(define cdro
  (lambda (p d)
    (fresh (a)
      (== (cons a d) p))))

(define conso
  (lambda (a d p)
    (== (cons a d) p)))

(define nullo
  (lambda (x)
    (== '() x)))

(define eqo
  (lambda (x y)
    (== x y)))

(define eq-caro
  (lambda (l x)
    (caro l x)))

(define pairo
  (lambda (p)
    (fresh (a d)
      (conso a d p))))

(define listo
  (lambda (l)
    (conde
      ((nullo l))
      ((pairo l)
       (fresh (d)
         (cdro l d)
         (listo d))))))

(define membero
  (lambda (x l)
    (conde
      ((eq-caro l x))
      ((fresh (d)
         (cdro l d)
         (membero x d))))))

(define rembero  
  (lambda (x l out)
    (conde
      ((nullo l) (== '() out))
      ((eq-caro l x) (cdro l out))
      ((fresh (a d res)
         (conso a d l)
         (rembero x d res)
         (conso a res out))))))

(define appendo
  (lambda (l s out)
    (conde
      ((nullo l) (== s out))
      ((fresh (a d res)
         (conso a d l)
         (conso a res out)
         (appendo d s res))))))

(define anyo
  (lambda (g)
    (conde
      (g)
      ((anyo g)))))

(define fail (== 'war 'peace))
(define succeed (== 'a 'a))

(define nevero (anyo fail))
 
(define alwayso (anyo succeed))

grammar

;; constructing sentences using relations

(define (conso car cdr c) (== `(,car . ,cdr) c))

(define (membero x l)
 (fresh (head tail)
  (== l `(,head . ,tail))
  (conde
   ((== x head))
   ((membero x tail)))))

(define (nouno n) (membero n '(cat bat)))
(define (verbo v) (membero v '(eats)))
(define (deto d)  (membero d '(the a)))

;; fixed sentence structure
(define (my-sentenceo s)
  (fresh (v n1 d1 n2 d2)
    (verbo v)
    (nouno n1)
    (nouno n2)
    (deto d1)
    (deto d2)
    (== s `(,d1 ,n1 ,v ,d2 ,n2))))

(my-sentenceo x)

;; with parameterized structure
(define (wordo class word)
 (conde
  ((== class 'noun) (nouno word))
  ((== class 'verb) (verbo word))
  ((== class 'det)  (deto word))))

(define (sentenceo grammar s)
 (conde ((== grammar '()) (== s '()))
        ((fresh (g-head s-head
                 g-tail s-tail)
           (conso g-head g-tail grammar)
           (conso s-head s-tail s)
           (wordo g-head s-head)
           (sentenceo g-tail s-tail)))))

(sentenceo '(det noun verb det noun) s)