Looking through the logs for an elegant to pull up (simplify) nested boolean logic. For example, a program like this:

(and aa (and bb cc) dd (or ee (and ff))

(and aa bb cc dd (or ee ff))

(m/rewrite
    program

    ;; single arg and/or unnest
    ((m/or and or) ?single-arg)
    ?single-arg

    ;; pull up nested ands, recursively
    (and . (m/or (m/cata (and . !arg ...)) (m/cata !arg)) ...)
    (and . !arg ...)

    ;; recurse
    ((m/cata !x) ...)
    (!x ...)

    ;; stop
    ?x ?x)

Something like that could probably work. When I’ve made logic simplifiers in the past, I always followed a structure like this. Made it nice and explicit what the rules for simplification were imo.

(defn reduce-logic [prop]
  (m/rewrite prop
    (or true ?x) true
    (or ?x true) true
    (or false ?x) ?x
    (or ?x false) ?x
    ?x ?x))

(defn recursive-reduce [prop]
  (m/match prop
    (?op ?x ?y) (reduce-logic (list ?op (recursive-reduce ?x) (recursive-reduce ?y)))
    (?op ?x) (reduce-logic (list ?op (recursive-reduce ?x)))
    ?x ?x))

(recursive-reduce '(or true true))
(recursive-reduce '(or true x))
(recursive-reduce '(or false x))
(recursive-reduce '(or (or (or false false) x) false))
(recursive-reduce '(or (or (or true false) x) false))

Oh, nice, I dig the explicit recursion. Seems easy to follow

Yeah, that is always the tricky bit is not infinite looping. This structure prevents you from having to think about that. In, fact I actually have an unnecessary cata. Let me remove that

Yeah, so everything in reduce-logic does not recurse at all. It is just the basic rules for simplification.