diff options
Diffstat (limited to 'scheme/mkdefs.scm')
| -rw-r--r-- | scheme/mkdefs.scm | 418 |
1 files changed, 418 insertions, 0 deletions
diff --git a/scheme/mkdefs.scm b/scheme/mkdefs.scm new file mode 100644 index 0000000..10ee052 --- /dev/null +++ b/scheme/mkdefs.scm @@ -0,0 +1,418 @@ + +; miniKanren prelude from simple-miniKanren + +; https://minikanren.org +; https://github.com/miniKanren/simple-miniKanren + + +(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) + (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 pairo + (lambda (p) + (fresh (a d) + (conso a d p)))) + +(define membero + (lambda (x l) + (conde + ((fresh (a) + (caro l a) + (== a x))) + ((fresh (d) + (cdro l d) + (membero x d)))))) + +(define rembero + (lambda (x l out) + (conde + ((nullo l) (== '() out)) + ((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 flatteno + (lambda (s out) + (conde + ((nullo s) (== '() out)) + ((pairo s) + (fresh (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) + (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 + ((nullo q) (pairo p)) + ((fresh (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)) + ((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 '()))) |