 (defmulti make-lattice-nc
   "Creates a new lattice from the given arguments, without any
   checks. Use with care."
-  {:arglists '([base-set order-function] [base-set inf sup])}
+  {:arglists '([base-set order-function]
+               [base-set inf sup]
+               [base-set order-function inf sup])}
   (fn [& args] (vec (map clojure-type args))))
 
 (defmethod make-lattice-nc [clojure-coll clojure-coll] [base-set order]

(defn modular?
  "Checks (primitively) whether given lattice lat is modular or not."
  [lat]
  (let [inf  (inf lat)
        sup  (sup lat)
        base (base-set lat)
        ordr (order lat)]
    (forall [x base
             y base
             z base]
      (=> (ordr [x z])
          (= (sup x (inf y z))
             (inf (sup x y) z))))))

(defn lattice-one
  "Returns the one element of lattice lat."
  [lat]
  (let [order (order lat)
        base  (base-set lat)]
    (first (set-of x [x base :when (forall [y base] (order [y x]))]))))

(defn lattice-zero
  "Returns the zero element of lattice lat."
  [lat]
  (let [order (order lat)
        base  (base-set lat)]
    (first (set-of x [x base :when (forall [y base] (order [x y]))]))))

(defn directly-neighboured?
  "Checks whether x is direct lower neighbour of y in lattice lat."
  [lat x y]
  (let [order (order lat)
        base  (base-set lat)]
    (and (not= x y)
         (order [x y])
         (forall [z base]
           (=> (and (not= z x) (not= z y))
               (not (and (order [x z])
                         (order [z y]))))))))

(defn lattice-upper-neighbours
  "Returns all direct upper neighbours of x in lattice lat."
  [lat x]
  (set-of y [y (base-set lat) :when (directly-neighboured? lat x y)]))

(defn lattice-lower-neighbours
  "Returns all direct lower neighbours of y in lattice lat."
  [lat y]
  (set-of x [x (base-set lat) :when (directly-neighboured? lat x y)]))

(defn lattice-atoms
  "Returns the lattice atoms of lat."

  (intersection (lattice-sup-irreducibles lat)
                (lattice-inf-irreducibles lat)))

(defn lattice-heights
  "Returns a function giving for every element in the base-set of the
  given lattice its height."
  [lat]
  (let [zero (lattice-zero lat),
        maxi (count (base-set lat)),
        heig (memo-fn h [x]
               (if (= x zero)
                 0
                 (inc (reduce (fn [mi a]
                                (if (directly-neighboured? lat a x)
                                  (min mi (h a))
                                  mi))
                              maxi
                              (disj (base-set lat) x)))))]
    (fn [x]
      (when-not (contains? (base-set lat) x)
        (illegal-argument "Given element is not contained in lattice."))
      (heig x))))

;;; FCA

