                                     :abort))]
             (cond
              (= counterexamples :abort)
-             (recur implications nil ctx) ;; forget all other sets
-             ;;;
+             (recur implications nil ctx) ; forget all other sets
+             ;;
              counterexamples
              (let [new-objs (map first counterexamples)]
                ;; check that new names are not there already

(ns-doc
 "Provides function for exploration and computing proper premises.")

;;; Attribute Exploration

(declare default-handler)

(defnk explore-attributes
  "Performs attribute exploration in given context. Returns a hashmap

                                    (union (incidence ctx)
                                           (set-of [g m] [[g ms] counterexamples,
                                                          m ms])))))
             ;;
             true                       ; add counterexample
             (recur (conj implications new-impl)
                    (next-closed-set (attributes ctx)
                                     (clop-by-implications (conj implications new-impl))
                                     last)
                    ctx))))))))

;;; Attribute Exploration with Incomplete Counterexamples

(let [dh (make-handler :incomplete-counterexamples? true)]
  (defn default-handler-for-incomplete-counterexamples
    "Default handler for attribute exploration with incomplete counterexamples. Does it's
    interaction on the console."
    [possible-ctx certain-ctx known impl]
    (dh possible-ctx certain-ctx known impl)))

(defnk explore-attributes-with-incomplete-counterexamples
  "EXPERIMENTAL and LARGLY UNTESTED — USE WITH CARE

  Performs attribute exploration in given contexts of possible («possible-ctx») and
  certain («certain-ctx») incidences, allowing the expert to provide incomplete
  counterexamples.  Returns a hashmap of implications computed and the final context,
  stored with keys :implications and :context, respectively.

  The function takes a number of keyword arguments, which are as follows:

  - :handler «fn»

    Interaction is accomplished via the given handler fn, which is called
    with the current context of possible incidences, the current context of
    certain indcidences, all implications known so far and a new
    implication. The handler has to return counterexamples for the new
    implication, if there are some. Otherwise it has to return
    nil. Counterexamples are given as a sequence of rows, every row being
    of the form

       [g positive-attributes negative-attributes],

    where «g» is a new object, «positive-attributes» is a sequence of
    attributes the new object has, and «negative-attributes» is a sequence
    of attributes the new object does not have.  Note that
    «positive-attributes» and «negative-attributes» must be disjoint.

  - :background-knowledge «set of implications»

    background-knowledge denotes a set of implications used as
    background knowledge, which will be subtracted from the computed
    result.

  If you want to use automorphisms of the underlying context, you have
  to construct a special handler using the «make-handler»
  function. See the corresponding documentation of «make-handler»."
  [possible-ctx, certain-ctx,
   :background-knowledge #{},
   :handler default-handler-for-incomplete-counterexamples]
  (assert (set? background-knowledge))
  (assert (= (attributes certain-ctx)
             (attributes possible-ctx))
          "Given contexts must coincide on the set of attributes")
  (assert (= (objects certain-ctx)
             (objects possible-ctx))
          "Given contexts must coincide on the set of objects")
  (loop [implications background-knowledge,
         last         (close-under-implications implications #{}),
         possible-ctx possible-ctx
         certain-ctx  certain-ctx]
    (if (not last)
      {:implications (difference implications background-knowledge),
       :possible-context possible-ctx
       :certain-context  certain-ctx}
      (let [conclusion-from-last (oprime possible-ctx (aprime certain-ctx last))] ; ?
        (if (= last conclusion-from-last)
          (recur implications
                 (next-closed-set (attributes possible-ctx)
                                  (clop-by-implications implications)
                                  last)
                 possible-ctx
                 certain-ctx)
          (let [new-impl        (make-implication last conclusion-from-last),
                counterexamples (try
                                  (handler possible-ctx certain-ctx implications new-impl)
                                  (catch Throwable e
                                    :abort))]

            (cond
             (= counterexamples :abort)
             (recur implications nil possible-ctx certain-ctx) ; abort exploration
             ;;
             counterexamples            ; add counterexample
             (let [new-objs (map first counterexamples)]
               ;; check that new names are not there already
               (when (exists [g new-objs] (contains? (objects possible-ctx) g))
                 (illegal-argument "Got objects as «new objects» in exploration "
                                   "which are already present."))
               (recur implications
                      last
                      ;; possible incidence, i.e. the one not excluded by the expert
                      (make-context (into (objects possible-ctx) new-objs)
                                    (attributes possible-ctx)
                                    (union (incidence possible-ctx)
                                           (set-of [g m] | [g _ neg] counterexamples
                                                           m (difference (attributes possible-ctx)
                                                                         (set neg)))))
                      ;; certain incidence, i.e. the one given by the expert
                      (make-context (into (objects certain-ctx) new-objs)
                                    (attributes certain-ctx)
                                    (union (incidence certain-ctx)
                                           (set-of [g m] [[g pos _] counterexamples,
                                                          m pos])))))
             ;;
             true                       ; add implication
             (let [new-implications (conj implications new-impl)]
               (recur new-implications
                      (next-closed-set (attributes possible-ctx)
                                       (clop-by-implications new-implications)
                                       last)
                      possible-ctx
                      (make-context (objects certain-ctx)
                                    (attributes certain-ctx)
                                    (set-of [g m] | g (objects certain-ctx)
                                                    m (close-under-implications
                                                       new-implications
                                                       (oprime certain-ctx #{g})))))))))))))

;;;

