Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
148 lines (95 sloc) 1.75 KB
(import [mk [*]])
(require mk)
(defn append [l r]
(cond
[(= l []) r]
[True
(cons (car l) (append (cdr l) r))]))
(defn appendo [l r out]
(conde
[(== l []) (== r out)]
[(fresh [a d res]
(== (cons a d) l)
(== (cons a res) out)
(appendo d r res))]))
[[[], [1 2 3 4]],
[[1], [2 3 4]],
[[1 2], [3 4]],
[[1 2 3], [4]],
[[1 2 3 4], []]]
;; TOP SLIDES
;; SLIDE 26
(run*
(fresh [q]
(== q 5)))
;; SLIDE 27
(run*
(fresh [q]
(== 1 1)))
;; SLIDE 28
(run*
(fresh [q]
(== 1 2)))
;; SLIDE 29
(run*
(fresh [x y]
(== y 6)
(== x y)))
;; SLIDE 30
(run*
(fresh [q]
(conde [(== q 5)]
[(== q 6)])))
;; SLIDE 31
(run*
(fresh [x y]
(conde [(== y 5) (== x y)]
[(== x 6)])))
;; SLIDE 32
(defn caro [p a]
(fresh [d]
(== (cons a d) p)))
(defn cdro [p d]
(fresh [a]
(== (cons a d) p)))
(defn conso [a d p]
(== (cons a d) p))
(defn nullo [x]
(== [] x))
;; SLIDE 33
(defn appendo [l r out]
(conde
((== [] l) (== r out))
((fresh [a d res]
(== (cons a d) l)
(== (cons a res) out)
(appendo d r res)))))
(run*
(fresh [q]
(appendo [1 2] [3 4] q)))
(run*
(fresh [q]
(appendo [1 2] q [1 2 3 4])))
;; SLIDE 34
(run*
(fresh [q x y]
(appendo x y [1 2 3 4])))
(run*
(fresh [q x y]
(appendo x y [1 2 3 4])
(== [x y] q)))
;; SLIDE 35
(defn append [l r]
"Join two lists"
(cond
[(= l []) r]
[True
(cons (car l) (append (cdr l) r))]))
;; SLIDE 36
(defn appendo [l r out]
(conde
[(== [] l) (== r out)]
[(fresh [a d res]
(== (cons a d) l)
(== (cons a res) out)
(appendo d r res))]))