WIP

README.md

@@ -7,7 +7,7 @@ TODO: need a better name
 Certora Collections provides data structure implementations for Kotlin that are designed for efficient functional programming.
 These data structures are immutable and persistent, and designed for minimal memory usage when used in a functional
 style. They also include other features that we have found helpful in implementing the Certora Prover, such as efficient
-joining/merging of maps, parallel operations, etc.  
+joining/merging of maps, parallel operations, etc.
 
 We build on the interfaces introduced in
 [kotlinx.collections.immutable](https://github.com/Kotlin/kotlinx.collections.immutable), but provide a different

collect/src/main/kotlin/com/certora/collect/Treap.kt

@@ -36,9 +36,7 @@ package com.certora.collect
     keys in Maps.  For types that do not implement Comparable, we use the object's hashCode() function to generate a
     Treap key.  We thus sort all elements/keys by their hash codes.  We resolve collisions by chaining off of the Treap
     node.  This results in a bifurcation of Set and Map implementations, into SortedTreapSet and HashTreapSet,
-    SortedTreapMap and HashTreapMap.  To make this more manageable at use sites, we We provide AutoPersistentSet and
-    AutoPersistentMap, which are empty set/map objects that expand into the appropriate sorted/hashed structure based on
-    the actual key types encountered.
+    SortedTreapMap and HashTreapMap.
 
     Some other notes:
 
@@ -55,10 +53,8 @@ package com.certora.collect
     - To ensure "persistence" of these data structures, all instances of Treap are deeply immutable.  "Mutation" is
       always done by making a new instance.  We go to lengths to avoid this, and also to throw out any copies if they
       turn out to be unnecessary, so that we maximize our chances of reusing existing memory allocations, in the hope of
-      keeping memory small.  Typically a union of two Sets, for example, will reuse a substantial portion of both sets.
-
-    - Most Treap operations are written as extension methods, so that they can deal with null "this" values.  This makes
-      things much more convenient, but is a bit odd, and is another reason this stuff is isolated in its own package.
+      keeping memory small.  Often a union of two large Sets, for example, will reuse a substantial portion of both
+      sets.
 
     - Most Treap operations are defined recursively.  This should not lead to stack overflow, as Treaps are very likely
       to be mostly balanced.  The expected (ideal) depth of a Treap is O(log2(N)), so we don't expect to see Treaps that

collect/src/main/kotlin/com/certora/collect/TreapKey.kt

@@ -62,7 +62,7 @@ internal interface TreapKey<@Treapable K> {
     abstract fun precompute(): TreapKey<K>
 
     /**
-        A TreapKey whose underlying key implement Comparable.  This allows us to sort the Treap naturally.
+        A TreapKey whose underlying key implements Comparable.  This allows us to sort the Treap naturally.
      */
     interface Sorted<@Treapable K : Comparable<K>> : TreapKey<K> {
         abstract override val treapKey: K

collect/src/main/kotlin/com/certora/collect/Treapable.kt

@@ -6,17 +6,17 @@ package com.certora.collect
     The internal structure of Treap-based collections is based on the hash codes of the keys stored in the collection.
     If a Treap is serialized and deserialized, the hash codes of the keys must be the same as they were before
     serialization, or the Treap will be corrupted.  To prevent this, we use [Treapable] annotations to convey hash code
-    stability requirements, and optionally enforce these requirements with the [Treapability] Detekt rule. 
+    stability requirements, and optionally enforce these requirements with the [Treapability] Detekt rule.
 
     A type parameter annotated with [Treapable] requires that all arguments to the type parameter have stable hash code
-    *if* they are also possibly serializable.  
+    *if* they are also possibly serializable.
 
     A type is definitely not serializable if it does not implement Serializable *and* it is final (or sealed, and all
     subclasses are definitely not serializable).
 
     A class, interface, or object annotated with [Treapable] must have a stable hash code (and all subclasses must
     also).  The [Treapability] rule will report a violation if a class, interface, or object annotated with [Treapable]
-    does not appear to have a stable hash code.  
+    does not appear to have a stable hash code.
 
     The [Treapability] rule will also report a violation if an argument to a [Treapable] type parameter is potentially
     serializable and does not have a stable hash code.  Some notes on hash code stability:
@@ -41,7 +41,7 @@ package com.certora.collect
       and do not allow this to be overridden.  A stable hash code can be obtained from the *name* of the enum instance.
       (We could also use the ordinal, but this has an unnecessary dependence on ordering.)
 
-    - Our analysis considers some known JVM types to have stable hash codes (such as BigIngeter).
+    - Our analysis assumes some known JVM types to have stable hash codes (such as BigIngeter).
  */
 @Target(AnnotationTarget.TYPE_PARAMETER, AnnotationTarget.TYPE, AnnotationTarget.CLASS)
 public annotation class Treapable