            (println t)
            state))))))
 
+;;
+
 (defn counterexample-via-repl
-  "Starts a repl for counterexamples."
+  "Starts a repl for counterexamples, which must be specified completely."
   [ctx knowledge impl]
   (loop [state {:context ctx,
                 :knowledge knowledge,
-                :implication impl}]
+                :implication impl
+                :complete-counterexamples? true}]
     (let [query  (ask "counterexample> "
                       #(read-string (str (read-line)))
                       (constantly true)


(defn- valid-counterexample?
  "Checks the given example for being valid."
  [state ctx impl]
  (let [new-atts    (union (set (:positives state)) (set (:negatives state))),
        return      (atom true)]
    (when-not (contains? state :object),
      (println "You need to set a name for the new object.")
      (reset! return false))
    (when-not (= (attributes ctx) new-atts)
      (println "You have not specified a complete counterexample.")
      (reset! return false))
    (let [not-respected (filter (fn [impl]

        (recur result)
        [(:object state) (set (:positives state))]))))

(defn incomplete-counterexample-via-repl
  "Starts a repl for counterexamples, which may be incomplete."
  [possible-ctx certain-ctx knowledge impl]
  (loop [state {:possible-context possible-ctx,
                :certain-context certain-ctx,
                :knowledge knowledge,
                :implication impl
                :complete-counterexamples? false}]
    (let [query  (ask "counterexample> "
                      #(read-string (str (read-line)))
                      (constantly true)
                      "counterexample> "),
          result (eval-command query state)]
      (if result
        (recur result)
        [(:object state) (set (:positives state)) (set (:negatives state))]))))

;; REPL commands

(defmacro- define-repl-fn [name doc & body]
  `(do
     (defmethod run-repl-command '~name
       ~'[_ state]
       (let [~'objects    (objects (or (:context ~'state)
                                       (:possible-context ~'state)))
             ~'attributes (attributes (or (:context ~'state)
                                          (:possible-context ~'state))),
             ~'impl       (:implication ~'state)]
         ~@body))
     (defmethod help-repl-command '~name
       ~'[_]
