(ns locus.order.lattice.term.identities
  (:require [locus.set.logic.core.set :refer :all]
            [locus.set.logic.limit.product :refer :all]
            [locus.set.mapping.general.core.object :refer :all]
            [locus.set.logic.structure.protocols :refer :all]
            [locus.set.copresheaf.structure.core.protocols :refer :all]
            [locus.set.quiver.relation.binary.product :refer :all]
            [locus.order.general.core.object :refer :all]
            [locus.order.lattice.core.object :refer :all]
            [locus.order.lattice.term.lattice-term :refer :all]
            [locus.set.quiver.structure.core.protocols :refer :all])
  (:import (locus.order.lattice.core.object Lattice)
           (locus.order.lattice.term.lattice_term LatticeTerm)))

; Let L be a distributive lattice, then the lattice terms in L satisfy
; the meet and join distributive laws. These can be used to convert lattice
; expressions into either join or meet normal forms. In order to implement these
; normalisation routines over arbitrary lattices we provide additional functions
; that handle lattice terms and expressions.

; Meet distribution of lattice polynomial expressions
(defn meet-distribute-once
  [expr]

  (if (multiplicative-expression? expr)
    (let [terms (rest expr)]
      (let [product-expressions (map
                                  (fn [i]
                                    (cons '* i))
                                  (apply
                                    enumerate-cartesian-product
                                    (map
                                      (fn [term]
                                        (if (not (coll? term))
                                          (list term)
                                          (rest term)))
                                      terms)))]
        (if (= (count product-expressions) 1)
          (first product-expressions)
          (cons '+ product-expressions))))
    expr))

; The main algorithm for producing meet normal forms of lattice expressions
(defn meet-distribute
  [expr]

  (cond
    ; if it is a singleton element then terminate and return
    (not (coll? expr)) expr

    ; a simple multiplicative expression cannot be distributed further
    ; so terminate the current algorithm and return
    (simple-multiplicative-expression? expr) expr

    ; in the other case we can try to perform meet distribution simplification
    (multiplicative-expression? expr)
    (let [current-simplification (simplify-lattice-expression (meet-distribute-once expr))]
      (meet-distribute current-simplification))

    ; additive expressions require simplification of all their terms
    (additive-expression? expr)
    (simplify-lattice-expression
      (cons
        '+
        (map
          (fn [i]
            (meet-distribute i))
          (rest expr))))))

 Let L be a distributive lattice, then the lattice terms in L satisfy
 the meet and join distributive laws. These can be used to convert lattice
 expressions into either join or meet normal forms. In order to implement these
 normalisation routines over arbitrary lattices we provide additional functions
 that handle lattice terms and expressions.
 Meet distribution of lattice polynomial expressions
 The main algorithm for producing meet normal forms of lattice expressions
 if it is a singleton element then terminate and return
 a simple multiplicative expression cannot be distributed further
 so terminate the current algorithm and return
 in the other case we can try to perform meet distribution simplification
 additive expressions require simplification of all their terms
(ns locus.order.lattice.term.identities
  (:require [locus.set.logic.core.set :refer :all]
            [locus.set.logic.limit.product :refer :all]
            [locus.set.mapping.general.core.object :refer :all]
            [locus.set.logic.structure.protocols :refer :all]
            [locus.set.copresheaf.structure.core.protocols :refer :all]
            [locus.set.quiver.relation.binary.product :refer :all]
            [locus.order.general.core.object :refer :all]
            [locus.order.lattice.core.object :refer :all]
            [locus.order.lattice.term.lattice-term :refer :all]
            [locus.set.quiver.structure.core.protocols :refer :all])
  (:import (locus.order.lattice.core.object Lattice)
           (locus.order.lattice.term.lattice_term LatticeTerm)))


(defn meet-distribute-once
  [expr]

  (if (multiplicative-expression? expr)
    (let [terms (rest expr)]
      (let [product-expressions (map
                                  (fn [i]
                                    (cons '* i))
                                  (apply
                                    enumerate-cartesian-product
                                    (map
                                      (fn [term]
                                        (if (not (coll? term))
                                          (list term)
                                          (rest term)))
                                      terms)))]
        (if (= (count product-expressions) 1)
          (first product-expressions)
          (cons '+ product-expressions))))
    expr))

(defn meet-distribute
  [expr]

  (cond
    (not (coll? expr)) expr

    (simple-multiplicative-expression? expr) expr

    (multiplicative-expression? expr)
    (let [current-simplification (simplify-lattice-expression (meet-distribute-once expr))]
      (meet-distribute current-simplification))

    (additive-expression? expr)
    (simplify-lattice-expression
      (cons
        '+
        (map
          (fn [i]
            (meet-distribute i))
          (rest expr))))))
