Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

414 lines (373 sloc) 11.489 kB
(load "mkneverequalo.scm")
(define-syntax run1 (syntax-rules () ((_ (x) g0 g ...) (run 1 (x) g0 g ...))))
(define-syntax run2 (syntax-rules () ((_ (x) g0 g ...) (run 2 (x) g0 g ...))))
(define-syntax run3 (syntax-rules () ((_ (x) g0 g ...) (run 3 (x) g0 g ...))))
(define-syntax run4 (syntax-rules () ((_ (x) g0 g ...) (run 4 (x) g0 g ...))))
(define-syntax run5 (syntax-rules () ((_ (x) g0 g ...) (run 5 (x) g0 g ...))))
(define-syntax run6 (syntax-rules () ((_ (x) g0 g ...) (run 6 (x) g0 g ...))))
(define-syntax run7 (syntax-rules () ((_ (x) g0 g ...) (run 7 (x) g0 g ...))))
(define-syntax run8 (syntax-rules () ((_ (x) g0 g ...) (run 8 (x) g0 g ...))))
(define-syntax run9 (syntax-rules () ((_ (x) g0 g ...) (run 9 (x) g0 g ...))))
(define-syntax run10 (syntax-rules () ((_ (x) g0 g ...) (run 10 (x) g0 g ...))))
(define-syntax run11 (syntax-rules () ((_ (x) g0 g ...) (run 11 (x) g0 g ...))))
(define-syntax run12 (syntax-rules () ((_ (x) g0 g ...) (run 12 (x) g0 g ...))))
(define-syntax run13 (syntax-rules () ((_ (x) g0 g ...) (run 13 (x) g0 g ...))))
(define-syntax run14 (syntax-rules () ((_ (x) g0 g ...) (run 14 (x) g0 g ...))))
(define-syntax run15 (syntax-rules () ((_ (x) g0 g ...) (run 15 (x) g0 g ...))))
(define-syntax run16 (syntax-rules () ((_ (x) g0 g ...) (run 16 (x) g0 g ...))))
(define-syntax run17 (syntax-rules () ((_ (x) g0 g ...) (run 17 (x) g0 g ...))))
(define-syntax run18 (syntax-rules () ((_ (x) g0 g ...) (run 18 (x) g0 g ...))))
(define-syntax run19 (syntax-rules () ((_ (x) g0 g ...) (run 19 (x) g0 g ...))))
(define-syntax run20 (syntax-rules () ((_ (x) g0 g ...) (run 20 (x) g0 g ...))))
(define-syntax run21 (syntax-rules () ((_ (x) g0 g ...) (run 21 (x) g0 g ...))))
(define-syntax run22 (syntax-rules () ((_ (x) g0 g ...) (run 22 (x) g0 g ...))))
(define-syntax run23 (syntax-rules () ((_ (x) g0 g ...) (run 23 (x) g0 g ...))))
(define-syntax run24 (syntax-rules () ((_ (x) g0 g ...) (run 24 (x) g0 g ...))))
(define-syntax run25 (syntax-rules () ((_ (x) g0 g ...) (run 25 (x) g0 g ...))))
(define-syntax run26 (syntax-rules () ((_ (x) g0 g ...) (run 26 (x) g0 g ...))))
(define-syntax run27 (syntax-rules () ((_ (x) g0 g ...) (run 27 (x) g0 g ...))))
(define-syntax run28 (syntax-rules () ((_ (x) g0 g ...) (run 28 (x) g0 g ...))))
(define-syntax run29 (syntax-rules () ((_ (x) g0 g ...) (run 29 (x) g0 g ...))))
(define-syntax run30 (syntax-rules () ((_ (x) g0 g ...) (run 30 (x) g0 g ...))))
(define-syntax run31 (syntax-rules () ((_ (x) g0 g ...) (run 31 (x) g0 g ...))))
(define-syntax run32 (syntax-rules () ((_ (x) g0 g ...) (run 32 (x) g0 g ...))))
(define-syntax run33 (syntax-rules () ((_ (x) g0 g ...) (run 33 (x) g0 g ...))))
(define-syntax run34 (syntax-rules () ((_ (x) g0 g ...) (run 34 (x) g0 g ...))))
(define-syntax run35 (syntax-rules () ((_ (x) g0 g ...) (run 35 (x) g0 g ...))))
(define-syntax run36 (syntax-rules () ((_ (x) g0 g ...) (run 36 (x) g0 g ...))))
(define-syntax run37 (syntax-rules () ((_ (x) g0 g ...) (run 37 (x) g0 g ...))))
(define-syntax run38 (syntax-rules () ((_ (x) g0 g ...) (run 38 (x) g0 g ...))))
(define-syntax run39 (syntax-rules () ((_ (x) g0 g ...) (run 39 (x) g0 g ...))))
(define-syntax run40 (syntax-rules () ((_ (x) g0 g ...) (run 40 (x) g0 g ...))))
(define caro
(lambda (p a)
(exist (d)
(== (cons a d) p))))
(define cdro
(lambda (p d)
(exist (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 pairo
(lambda (p)
(exist (a d)
(conso a d p))))
(define membero
(lambda (x l)
(conde
((exist (a)
(caro l a)
(== a x)))
((exist (d)
(cdro l d)
(membero x d))))))
(define rembero
(lambda (x l out)
(conde
((nullo l) (== '() out))
((caro l x) (cdro l out))
((exist (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))
((exist (a d res)
(conso a d l)
(conso a res out)
(appendo d s res))))))
(define flatteno
(lambda (s out)
(conde
((nullo s) (== '() out))
((pairo s)
(exist (a d res-a res-d)
(conso a d s)
(flatteno a res-a)
(flatteno d res-d)
(appendo res-a res-d out)))
((conso s '() out)))))
(define anyo
(lambda (g)
(conde
(g)
((anyo g)))))
(define nevero (anyo fail))
(define alwayso (anyo succeed))
(define build-num
(lambda (n)
(cond
((odd? n)
(cons 1
(build-num (quotient (- n 1) 2))))
((and (not (zero? n)) (even? n))
(cons 0
(build-num (quotient n 2))))
((zero? n) '()))))
(define poso
(lambda (n)
(exist (a d)
(== `(,a . ,d) n))))
(define >1o
(lambda (n)
(exist (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)
(exist (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)
(exist (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))
((exist (x z)
(== `(0 . ,x) n) (poso x)
(== `(0 . ,z) p) (poso z)
(>1o m)
(*o x m z)))
((exist (x y)
(== `(1 . ,x) n) (poso x)
(== `(0 . ,y) m) (poso y)
(*o m n p)))
((exist (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)
(exist (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
((nullo q) (pairo p))
((exist (x y z)
(cdro q x)
(cdro p y)
(conde
((nullo n)
(cdro m z)
(bound-*o x y z '()))
((cdro n z)
(bound-*o x y z m))))))))
(define =lo
(lambda (n m)
(conde
((== '() n) (== '() m))
((== '(1) n) (== '(1) m))
((exist (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))
((exist (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)
(exist (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)
(exist (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))
((exist (b n^)
(== `(0 ,b . ,n^) n)
(== '() r)
(== `(,b . ,n^) h)
(== '() l)))
((exist (n^)
(== `(1 . ,n^) n)
(== '() r)
(== n^ h)
(== '(1) l)))
((exist (b n^ a r^)
(== `(0 ,b . ,n^) n)
(== `(,a . ,r^) r)
(== '() l)
(splito `(,b . ,n^) r^ '() h)))
((exist (n^ a r^)
(== `(1 . ,n^) n)
(== `(,a . ,r^) r)
(== '(1) l)
(splito n^ r^ '() h)))
((exist (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)
(exist (a ad dd)
(poso dd)
(== `(,a ,ad . ,dd) n)
(exp2 n '() q)
(exist (s)
(splito n dd r s))))
((exist (a ad add ddd)
(conde
((== '(1 1) b))
((== `(,a ,ad ,add . ,ddd) b))))
(<lo b n)
(exist (bw1 bw nw nw1 ql1 ql s)
(exp2 b '() bw1)
(pluso bw1 '(1) bw)
(<lo q n)
(exist (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)
(exist (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)
(exist (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)
(exist (s)
(splito n b s '(1))))
((exist (q1 b2)
(== `(0 . ,q1) q)
(poso q1)
(<lo b n)
(appendo b `(1 . ,b) b2)
(exp2 n b2 q1)))
((exist (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)
(exist (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 '())))
Jump to Line
Something went wrong with that request. Please try again.