Compile-time verification of session-type-like programs in Clojure

sessions.clj

(require '[clojure.string :as str])
 
(defn parse [s]
  (->> s
       str/split-lines
       (map (fn [line]
              (let [[action source destination alternative]
                    (str/split (str/trim line) #" +")]
                [action
                 {:source source
                  :destination destination
                  :alternative alternative}])))
       (into {})))
 
(defmacro session [protocol-filename [initial-state final-state] & actions]
  (let [protocol (parse (slurp (io/resource protocol-filename)))
        valid-actions (set (keys protocol))
        valid-states (set (mapcat (juxt :source :destination) (vals protocol)))]
    (cond
      (not (valid-states initial-state))
      (throw (ex-info (str "Invalid initial state " initial-state)
                      {:valid-states valid-states}))
      (not (valid-states final-state))
      (throw (ex-info (str "Invalid final state " final-state)
                      {:valid-states valid-states}))
 
      :else
      (loop [state initial-state
             [action & nxt] actions]
        (if-not (valid-actions action)
          (throw (ex-info (str "Invalid action " action)
                          {:valid-actions valid-actions}))
          (let [{:keys [source destination]} (get protocol action)]
            (cond
              (not= source state)
              (throw (ex-info (str "Action " action " is not valid in state " state) {}))
 
              (seq nxt)
              (recur destination nxt)
 
              (not (= destination final-state))
              (throw (ex-info (str "Expected final state " final-state ", got " destination) {}))
 
              :else ; we're done! program is correct
              (into [] actions))))))))
 
;; At macro-expansion time, this session will be verified against the protocol
;; described in "vending-machine.txt", starting in state "waiting" and proving
;; that the session always ends in state "vended".
(session "vending-machine.txt" ["waiting" "vended"]
         ;; "hack" -> Won't compile as it's not a legal action described in vending-machine.txt
         "pay"
         "return"
         ;; "vend" -> Won't compile as it's not a legal action *in this state*.
         "pay"
         "select"
         "vend") ;; if you forgot "vend", it wouldn't compile either, as the final state of this session *must* be "vended"

vending-machine.txt

pay     waiting   paid      broken
return  paid      waiting   broken
select  paid      selected  broken
vend    selected  vended    broken