Kibit

class: center, middle
`(use 'clojure.core.logic)`

---

class: center, middle

# The Kibit rule system

Jonas Enlund

Helsinki, April 2013

---
# Kibit
---
# Kibit

* Kibit is a static code analyzer for Clojure
---
# Kibit

* Kibit is a static code analyzer for Clojure
* Implemented as a leiningen plugin
---
# Kibit

* Kibit is a static code analyzer for Clojure
* Implemented as a leiningen plugin
* Looks for code patterns with more idiomatic alternatives
---
# Kibit

* Kibit is a static code analyzer for Clojure
* Implemented as a leiningen plugin
* Looks for code patterns with more idiomatic alternatives
* The rule system is built with core.logic
---

```
$ lein kibit src/overtone/examples/compositions/jazz.clj

```
---
```
$ lein kibit src/overtone/examples/compositions/jazz.clj

At src/overtone/examples/compositions/jazz.clj:100:
Consider using:
  (if-not (zero? (mod beat 2))
    (dec n)
    (limit (+ n (rand-nth jazz-intervals)) maxbass minbass))
instead of:
  (if (not (zero? (mod beat 2)))
    (dec n)
    (limit (+ n (rand-nth jazz-intervals)) maxbass minbass))
```
---

```
$ lein kibit src/overtone/examples/compositions/jazz.clj

At src/overtone/examples/compositions/jazz.clj:100:
Consider using:
  (if-not (zero? (mod beat 2))
    (dec n)
    (limit (+ n (rand-nth jazz-intervals)) maxbass minbass))
instead of:
  (if (not (zero? (mod beat 2)))
    (dec n)
    (limit (+ n (rand-nth jazz-intervals)) maxbass minbass))

At src/overtone/examples/compositions/jazz.clj:114:
Consider using:
  (inc beat)
instead of:
  (+ beat 1)

```
---

```
$ lein kibit src/overtone/examples/compositions/jazz.clj

At src/overtone/examples/compositions/jazz.clj:100:
Consider using:
  (if-not (zero? (mod beat 2))
    (dec n)
    (limit (+ n (rand-nth jazz-intervals)) maxbass minbass))
instead of:
  (if (not (zero? (mod beat 2)))
    (dec n)
    (limit (+ n (rand-nth jazz-intervals)) maxbass minbass))

At src/overtone/examples/compositions/jazz.clj:114:
Consider using:
  (inc beat)
instead of:
  (+ beat 1)

At src/overtone/examples/compositions/jazz.clj:133:
Consider using:
  (let [start (+ 1 (metro))]
    (at (metro start) (rotater-on note vel))
    (apply-by (metro (+ len start)) #'rotater-off [note]))
instead of:
  (let [start (+ 1 (metro))]
    (do
      (at (metro start) (rotater-on note vel))
      (apply-by (metro (+ len start)) #'rotater-off [note])))
```
---

# Rules

```clojure
(defrules rules
  [(if (not ?pred) ?then ?else) (if-not ?pred ?then ?else)]
  [(+ ?x 1) (inc ?x)]
  [(let ?binding (do . ?body)) (let ?binding . ?body)]
  ;; etc ...
)
```
---

class: center middle
# Implementation details
(no prior knowledge of `core.logic` required)

---

# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
```
---
# Quick intro to core.logic
```clojure
(run* [q]
  (== 42 q))
;; (42)
```
---

# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
;; (42)

(run* [q]
  (== q '(+ 42 1)))
```
---
# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
;; (42)

(run* [q]
  (== q '(+ 42 1)))
;; ((+ 42 1))
```
---
# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
;; (42)

(run* [q]
  (== q '(+ 42 1)))
;; ((+ 42 1))

(run* [q]
  (== `(+ ~q 1) 
      `(+ 42 1)))
```
---
# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
;; (42)

(run* [q]
  (== q '(+ 42 1)))
;; ((+ 42 1))

(run* [q]
  (== `(+ ~q 1) 
      `(+ 42 1)))
;; (42)
```
---
# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
;; (42)

(run* [q]
  (== q '(+ 42 1)))
;; ((+ 42 1))

(run* [q]
  (== `(+ ~q 1) 
      `(+ 42 1)))
;; (42)

(run* [q]
  (fresh [x]
    (== `(+ ~x 1) 
        `(+ 42 1))
    (== `(inc ~x) q)))

```
---
# Quick intro to core.logic

```clojure
(run* [q]
  (== 42 q))
;; (42)

(run* [q]
  (== q '(+ 42 1)))
;; ((+ 42 1))

(run* [q]
  (== `(+ ~q 1) 
      `(+ 42 1)))
;; (42)

(run* [q]
  (fresh [x]
    (== `(+ ~x 1) 
        `(+ 42 1))
    (== `(inc ~x) q)))
;; ((clojure.core/inc 42))
```
---
# `(inc-rule <form>)`
---
# `(inc-rule <form>)`
```clojure
(defn inc-rule [form]
  (run* [q]
    (fresh [x]
      (== `(+ ~x 1) form)
      (== `(inc ~x) q))))
```
---
# `(inc-rule <form>)`

```clojure
(defn inc-rule [form]
  (run* [q]
    (fresh [x]
      (== `(+ ~x 1) form)
      (== `(inc ~x) q))))

(inc-rule `(+ 42 1))
```
---
# `(inc-rule <form>)`

```clojure
(defn inc-rule [form]
  (run* [q]
    (fresh [x]
      (== `(+ ~x 1) form)
      (== `(inc ~x) q))))

(inc-rule `(+ 42 1))
;; ((clojure.core/inc 42))
```
---
# `(inc-rule <form>)`

```clojure
(defn inc-rule [form]
  (run* [q]
    (fresh [x]
      (== `(+ ~x 1) form)
      (== `(inc ~x) q))))

(inc-rule `(+ 42 1))
;; ((clojure.core/inc 42))

(inc-rule `(map inc [1 2 3]))
```
---
# `(inc-rule <form>)`

```clojure
(defn inc-rule [form]
  (run* [q]
    (fresh [x]
      (== `(+ ~x 1) form)
      (== `(inc ~x) q))))

(inc-rule `(+ 42 1))
;; ((clojure.core/inc 42))

(inc-rule `(map inc [1 2 3]))
;; ()
```

---
# `((rule [<pattern> <subst>]) <form>)`
---
# `((rule [<pattern> <subst>]) <form>)`
```clojure
(defn rule [[patt subst]]
  (fn [form]
    (run* [q]
      (== patt form)
      (== subst q))))
```
---
# `((rule [<pattern> <subst>]) <form>)`
```clojure
(defn rule [[patt subst]]
  (fn [form]
    (run* [q]
      (== patt form)
      (== subst q))))

((rule [`(+ ~(lvar 'x false) 1) 
        `(inc ~(lvar 'x false))])
 `(+ 42 1))
```
---
# `((rule [<pattern> <subst>]) <form>)`
```clojure
(defn rule [[patt subst]]
  (fn [form]
    (run* [q]
      (== patt form)
      (== subst q))))

((rule [`(+ ~(lvar 'x false) 1) 
        `(inc ~(lvar 'x false))])
 `(+ 42 1))
;; ((clojure.core/inc 42))
```
---
# `((rule [<pattern> <subst>]) <form>)`
```clojure
(defn rule [[patt subst]]
  (fn [form]
    (run* [q]
      (== patt form)
      (== subst q))))

((rule [`(+ ~(lvar 'x false) 1) 
        `(inc ~(lvar 'x false))])
 `(+ 42 1))
;; ((clojure.core/inc 42))

(let [coll (lvar 'coll false)
      keys (lvar 'keys false)
      val  (lvar 'val  false)
      update-in-rule (rule [`(update-in ~coll ~keys assoc ~val)
                            `(assoc-in ~coll ~keys ~val)])
      form `(update-in {:x {:y 0}} [:x :z] assoc 0)]
  (update-in-rule form))
```
---
# `((rule [<pattern> <subst>]) <form>)`
```clojure
(defn rule [[patt subst]]
  (fn [form]
    (run* [q]
      (== patt form)
      (== subst q))))

((rule [`(+ ~(lvar 'x false) 1) 
        `(inc ~(lvar 'x false))])
 `(+ 42 1))
;; ((clojure.core/inc 42))

(let [coll (lvar 'coll false)
      keys (lvar 'keys false)
      val  (lvar 'val  false)
      update-in-rule (rule [`(update-in ~coll ~keys assoc ~val)
                            `(assoc-in ~coll ~keys ~val)])
      form `(update-in {:x {:y 0}} [:x :z] assoc 0)]
  (update-in-rule form))
;; ((clojure.core/assoc-in {:x {:y 0}} [:x :z] 0))
```
---
# Prepare for something better
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))
```
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))

(prepare '[(+ ?x 1) (inc ?x)])
```
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))

(prepare '[(+ ?x 1) (inc ?x)])
;; [(+ <lvar:?x> 1) (inc <lvar:?x>)]
```
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))

(prepare '[(+ ?x 1) (inc ?x)])
;; [(+ <lvar:?x> 1) (inc <lvar:?x>)]

((rule (prepare '[(+ ?x 1) (inc ?x)]))
 '(+ x 1))
```
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))

(prepare '[(+ ?x 1) (inc ?x)])
;; [(+ <lvar:?x> 1) (inc <lvar:?x>)]

((rule (prepare '[(+ ?x 1) (inc ?x)]))
 '(+ x 1))
;; ((inc x))
```
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))

(prepare '[(+ ?x 1) (inc ?x)])
;; [(+ <lvar:?x> 1) (inc <lvar:?x>)]

((rule (prepare '[(+ ?x 1) (inc ?x)]))
 '(+ x 1))
;; ((inc x))

((rule (prepare '[(update-in ?coll ?keys assoc ?val) 
                  (assoc-in ?coll ?keys ?val)]))
 '(update-in coll [:x :y] assoc 42))
```
---
# Prepare for something better
```clojure
(defn prepare [form]
  (walk/prewalk
   #(if (and (symbol? %)
             (.startsWith (name %) "?"))
      (lvar % false)
      %)
   form))

(prepare '[(+ ?x 1) (inc ?x)])
;; [(+ <lvar:?x> 1) (inc <lvar:?x>)]

((rule (prepare '[(+ ?x 1) (inc ?x)]))
 '(+ x 1))
;; ((inc x))

((rule (prepare '[(update-in ?coll ?keys assoc ?val) 
                  (assoc-in ?coll ?keys ?val)]))
 '(update-in coll [:x :y] assoc 42))
;; ((assoc-in coll [:x :y] 42))
```
---

# Rule v.2
---
# Rule v.2
```clojure
(defn rule [r]
  (let [r (prepare r)]
    (fn [form]  
      (run* [q]
        (fresh [patt subst]
          (== [patt subst] r)
          (== patt form)
          (== [form subst] q))))))
```
---
# Rule v.2
```clojure
(defn rule [r]
  (let [r (prepare r)]
    (fn [form]  
      (run* [q]
        (fresh [patt subst]
          (== [patt subst] r)
          (== patt form)
          (== [form subst] q))))))

((rule '[(+ ?x 1) (inc ?x)])
 '(+ 42 1))
```
---
# Rule v.2
```clojure
(defn rule [r]
  (let [r (prepare r)]
    (fn [form]  
      (run* [q]
        (fresh [patt subst]
          (== [patt subst] r)
          (== patt form)
          (== [form subst] q))))))

((rule '[(+ ?x 1) (inc ?x)])
 '(+ 42 1))
;; ([(+ 42 1) (inc 42)])
```
---
# Intermission: Meet membero
---
# Intermission: Meet membero
```clojure
(run* [q]
  (membero q [1 2 3 4]))
```
---
# Intermission: Meet membero
```clojure
(run* [q]
  (membero q [1 2 3 4]))
;; (1 2 3 4)
```
---
# Intermission: Meet membero
```clojure
(run* [q]
  (membero q [1 2 3 4]))
;; (1 2 3 4)

(run* [q]
  (membero 2 [1 q 3 4]))
```
---
# Intermission: Meet membero
```clojure
(run* [q]
  (membero q [1 2 3 4]))
;; (1 2 3 4)

(run* [q]
  (membero 2 [1 q 3 4]))
;; (2)
```
---
# Intermission: Meet membero
```clojure
(run* [q]
  (membero q [1 2 3 4]))
;; (1 2 3 4)

(run* [q]
  (membero 2 [1 q 3 4]))
;; (2)

(run* [q]
  (fresh [x y]
    (== x y)
    (membero x [1 2 3 4])
    (membero y [3 4 5 6])
    (== q [x y])))
```
---
# Intermission: Meet membero
```clojure
(run* [q]
  (membero q [1 2 3 4]))
;; (1 2 3 4)

(run* [q]
  (membero 2 [1 q 3 4]))
;; (2)

(run* [q]
  (fresh [x y]
    (== x y)
    (membero x [1 2 3 4])
    (membero y [3 4 5 6])
    (== q [x y])))
;; ([3 3] [4 4])
```
---
# rules, rules, rules!
---
# rules, rules, rules!
```clojure
(defn rules [rs]
  (let [rs (map prepare rs)]
    (fn [form]
      (run* [q]
        (fresh [patt subst]
          (membero [patt subst] rs)
          (== patt form)
          (== [form subst] q))))))
```

---
# rules, rules, rules!
```clojure
(defn rules [rs]
  (let [rs (map prepare rs)]
    (fn [form]
      (run* [q]
        (fresh [patt subst]
          (membero [patt subst] rs)
          (== patt form)
          (== [form subst] q))))))

(defmacro defrules
  [name & rs]
  `(def ~name
     (rules (quote ~rs))))
```

---
# rules, rules, rules!
```clojure
(defn rules [rs]
  (let [rs (map prepare rs)]
    (fn [form]
      (run* [q]
        (fresh [patt subst]
          (membero [patt subst] rs)
          (== patt form)
          (== [form subst] q))))))

(defmacro defrules
  [name & rs]
  `(def ~name
     (rules (quote ~rs))))

(defrules my-rules
  [(+ ?x 1) (inc ?x)]
  [(- ?x 1) (dec ?x)]
  [(< 0 ?x) (pos? ?x)]
  [(< ?x 0) (neg? ?x)]
  [(if ?test ?else nil) (when ?test ?else)]
  [(into [] ?coll) (vec ?coll)]
  [(apply concat (map ?f ?xs)) (mapcat ?f ?xs)])
```
---
# Test run
---
# Test run
```clojure
(my-rules '(if (some f xs) f nil))
```
---
# Test run
```clojure
(my-rules '(if (some f xs) f nil))
;; ([(if (some f xs) f nil) (when (some f xs) f)])
```
---
# Test run
```clojure
(my-rules '(if (some f xs) f nil))
;; ([(if (some f xs) f nil) (when (some f xs) f)])

(my-rules '(fn [x] 
             (if (< x 0) 
               (+ x 1)
               nil)))
```
---
# Test run
```clojure
(my-rules '(if (some f xs) f nil))
;; ([(if (some f xs) f nil) (when (some f xs) f)])

(my-rules '(fn [x] 
             (if (< x 0) 
               (+ x 1)
               nil)))
;; ()
```
---
# tree-seq and membero
---
# tree-seq and membero
```clojure
(tree-seq sequential? seq '(map (fn [x y] (+ x y)) xs))
```
---
# tree-seq and membero
```clojure
(tree-seq sequential? seq '(map (fn [x y] (+ x y)) xs))
;; ((map (fn [x y] (+ x y)) xs), 
;;  map, (fn [x y] (+ x y)), fn, 
;;  [x y], x, y, (+ x y), +, x 
;;  y, xs)
```
---
# tree-seq and membero
```clojure
(tree-seq sequential? seq '(map (fn [x y] (+ x y)) xs))
;; ((map (fn [x y] (+ x y)) xs), 
;;  map, (fn [x y] (+ x y)), fn, 
;;  [x y], x, y, (+ x y), +, x 
;;  y, xs)

(defn rules [rs]
  (let [rs (map prepare rs)]
    (fn [form]
      (run* [q]
        (fresh [patt subst subform]
          (membero [patt subst] rs)
          (membero subform (tree-seq sequential? seq form))
          (== patt subform)
          (== [subform subst] q))))))

```
---
# tree-seq and membero
```clojure
(tree-seq sequential? seq '(map (fn [x y] (+ x y)) xs))
;; ((map (fn [x y] (+ x y)) xs), 
;;  map, (fn [x y] (+ x y)), fn, 
;;  [x y], x, y, (+ x y), +, x 
;;  y, xs)

(defn rules [rs]
  (let [rs (map prepare rs)]
    (fn [form]
      (run* [q]
        (fresh [patt subst subform]
          (membero [patt subst] rs)
          (membero subform (tree-seq sequential? seq form))
          (== patt subform)
          (== [subform subst] q))))))

(my-rules '(fn [x] 
             (if (< x 0) 
               (+ x 1)
               nil))
```
---
# tree-seq and membero
```clojure
(tree-seq sequential? seq '(map (fn [x y] (+ x y)) xs))
;; ((map (fn [x y] (+ x y)) xs), 
;;  map, (fn [x y] (+ x y)), fn, 
;;  [x y], x, y, (+ x y), +, x 
;;  y, xs)

(defn rules [rs]
  (let [rs (map prepare rs)]
    (fn [form]
      (run* [q]
        (fresh [patt subst subform]
          (membero [patt subst] rs)
          (membero subform (tree-seq sequential? seq form))
          (== patt subform)
          (== [subform subst] q))))))

(my-rules '(fn [x] 
             (if (< x 0) 
               (+ x 1)
               nil))
;; ([(+ x 1) (inc x)] 
;;  [(< x 0) (neg? x)] 
;;  [(if (< x 0) (+ x 1) nil) (when (< x 0) (+ x 1))])
```
---
# Simplify
```clojure
(defn simplify* [form rules-fn]
  (walk/prewalk-replace (into {} (rules-fn form))
                        form))
```
---
# Simplify
```clojure
(defn simplify* [form rules-fn]
  (walk/prewalk-replace (into {} (rules-fn form))
                        form))

(simplify* '(fn [x] 
              (if (< x 0) 
                (+ x 1)
                nil))
           my-rules)
```
---
# Simplify
```clojure
(defn simplify* [form rules-fn]
  (walk/prewalk-replace (into {} (rules-fn form))
                        form))

(simplify* '(fn [x] 
              (if (< x 0) 
                (+ x 1)
                nil))
           my-rules)

;; (fn [x] 
;;   (when (neg? x) 
;;     (inc x)))
```
---
# Simplify
```clojure
(defn simplify* [form rules-fn]
  (walk/prewalk-replace (into {} (rules-fn form))
                        form))

(simplify* '(defn my-fun [xs]
              (apply concat 
                     (map (fn [x]
                            (into [] (if (< x 0)
                                       [(- x 1) (+ x 1)]
                                       nil)))
                          xs)))
           my-rules)
```
---
# Simplify
```clojure
(defn simplify* [form rules-fn]
  (walk/prewalk-replace (into {} (rules-fn form))
                        form))

(simplify* '(defn my-fun [xs]
              (apply concat 
                     (map (fn [x]
                            (into [] (if (< x 0)
                                       [(- x 1) (+ x 1)]
                                       nil)))
                          xs)))
           my-rules)

;; (defn my-fun [xs] 
;;   (mapcat (fn [x] 
;;             (vec (when (neg? x) 
;;                    [(dec x) (inc x)]))) 
;;           xs))
```
---
# Recursive rules
```clojure
(defrules max-rule
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))])
```
---
# Recursive rules
```clojure
(defrules max-rule
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))])

(simplify* '(max (s (s (s z))) 
                 (s (s (s (s (s z))))))
           max-rule)
```
---
# Recursive rules
```clojure
(defrules max-rule
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))])

(simplify* '(max (s (s (s z))) 
                 (s (s (s (s (s z))))))
           max-rule)
;; (s (max (s (s z))
;;         (s (s (s (s z))))))
```
---
# Recursive rules
```clojure
(defrules max-rule
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))])

(simplify* '(max (s (s (s z))) 
                 (s (s (s (s (s z))))))
           max-rule)
;; (s (max (s (s z))
;;         (s (s (s (s z))))))

(defn simplify [form rules-fn]
  (loop [form form]
    (let [new-form (simplify* form rules-fn)]
      (if (= new-form form)
        form
        (recur form)))))
```
---
# Recursive rules
```clojure
(defrules max-rule
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))])

(simplify* '(max (s (s (s z))) 
                 (s (s (s (s (s z))))))
           max-rule)
;; (s (max (s (s z))
;;         (s (s (s (s z))))))

(defn simplify [form rules-fn]
  (loop [form form]
    (let [new-form (simplify* form rules-fn)]
      (if (= new-form form)
        form
        (recur form)))))

(simplify '(max (s (s (s z))) 
                (s (s (s (s (s z))))))
          max-rule)

```
---
# Recursive rules
```clojure
(defrules max-rule
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))])

(simplify* '(max (s (s (s z))) 
                 (s (s (s (s (s z))))))
           max-rule)
;; (s (max (s (s z))
;;         (s (s (s (s z))))))

(defn simplify [form rules-fn]
  (loop [form form]
    (let [new-form (simplify* form rules-fn)]
      (if (= new-form form)
        form
        (recur form)))))

(simplify '(max (s (s (s z))) 
                (s (s (s (s (s z))))))
          max-rule)
;; (s (s (s (s (s z)))))

```
---
# Insertion sort
```clojure
(defrules insertion-sort
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))]
  [(min z ?x) z]
  [(min ?x z) z]
  [(min (s ?x) (s ?y)) (s (min ?x ?y))]
  [(sort nil) nil]
  [(sort (cons ?x ?y)) (insert ?x (sort ?y))]
  [(insert ?x nil) (cons ?x nil)]
  [(insert ?x (cons ?y ?z)) (cons (min ?x ?y) (insert (max ?x ?y) ?z))])
```
---
# Insertion sort
```clojure
(defrules insertion-sort
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))]
  [(min z ?x) z]
  [(min ?x z) z]
  [(min (s ?x) (s ?y)) (s (min ?x ?y))]
  [(sort nil) nil]
  [(sort (cons ?x ?y)) (insert ?x (sort ?y))]
  [(insert ?x nil) (cons ?x nil)]
  [(insert ?x (cons ?y ?z)) (cons (min ?x ?y) (insert (max ?x ?y) ?z))])

(simplify '(sort (cons (s (s z)) 
                       (cons (s z) 
                             (cons (s (s (s z))) 
                                   (cons z nil)))))
          insertion-sort)
```
---
# Insertion sort
```clojure
(defrules insertion-sort
  [(max z ?x) ?x]
  [(max ?x z) ?x]
  [(max (s ?x) (s ?y)) (s (max ?x ?y))]
  [(min z ?x) z]
  [(min ?x z) z]
  [(min (s ?x) (s ?y)) (s (min ?x ?y))]
  [(sort nil) nil]
  [(sort (cons ?x ?y)) (insert ?x (sort ?y))]
  [(insert ?x nil) (cons ?x nil)]
  [(insert ?x (cons ?y ?z)) (cons (min ?x ?y) (insert (max ?x ?y) ?z))])

(simplify '(sort (cons (s (s z)) 
                       (cons (s z) 
                             (cons (s (s (s z))) 
                                   (cons z nil)))))
          insertion-sort)
;; (cons z 
;;       (cons (s z) 
;;             (cons (s (s z)) 
;;                   (cons (s (s (s z))) 
;;                         nil))))
```
---
class: center middle
# Thanks for listening!
# ?questions

code: [`https://github.com/jonase/kibit-demo`](https://github.com/jonase/kibit-demo)

slides: [`http://jonase.github.io/kibit-demo`](http://jonase.github.io/kibit-demo)
   
More about term rewriting systems (TRS):

[`http://rewriting.loria.fr`](http://rewriting.loria.fr)