 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Implicit Set Protocol ;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defprotocol ImplicitStateSet
+;; Protocol used to represent both state sets, and value sets.
+;; State sets are like states, where the values implement PSet.
+;; Should also implement proper equality
+(defprotocol PSet
   (empty?    [s] "Is this set empty")
-;  (singleton-val [s v] "Return single possible value for far, or nil if not singleton")
   (singleton [s] "Return the singleton element making up this set, or nil if cardinality != 1.")
   (some-element [s] "Return an arbitrary element of this set, or throw if empty. ")
   (explicit-set [s] "Return an explicit outcome set. ")
-  (constrain [ss constraint] "Apply a constraint."))
-
+  (constrain [ss constraint] "Apply a constraint.")
+  (as-constraint [ss] "Return a constraint view.")
+  (subset? [s1 s2] "Is this set a (possibly improper) subset of the other?"))
+
+;; Allow Clojure sets to be used as value sets.
+(extend-type clojure.lang.IPersistentSet
+  PSet
+  (empty? [s] (clojure.core/empty? s))
+  (singleton [s] (util/singleton s))
+  (some-element [s]
+    (assert (not (clojure.core/empty? s)))
+    (first s))
+  (explicit-set [s] s)
+  (constrain [s constraint]
+    (assert (set? constraint))
+    (clojure.set/intersection s constraint))
+  (as-constraint [s] s)
+  (subset? [s1 s2] (util/subset? s1 s2)))
+
+
+(defn assert-pset! [x]
+  nil #_ (assert (satisfies? PSet x)))
+
+(defn proper-subset? [s1 s2]
+  (and (subset? s1 s2) (not (= s1 s2))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;; Factored Implicit Sets ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; for now, we can just require that these be unconditional.
;; If we add unions, etc later, worry about details.
;; TODO: constraint is not the same as set-vars ?  ???

;(def no-effect ::no-effect)

(declare make-logging-factored-state-set)


         (meta (first lfss))))))

(defn vars-known? [ss vars]
  (every? #(singleton (state/get-var ss %)) vars))

(defn get-known-var [ss var] (util/make-safe (singleton (state/get-var ss var))))

(defn ss-str [ss] "LFSS" (print-str (dissoc (state/as-map ss) :const)))
(defmethod print-method LoggingFactoredStateSet [ss o] (print-method (ss-str ss) o))




