package jazz.unsafe;

///////////////////////////////////////////////////////////////////////////////
//
//                  Iimperative implementation of hashtables
//
// Keys should be either of a numeric type or a string. Elements can be of any
// type, and the static type of the elements returned by "get" is the empty
// type that can be cast into any type as needed. Type-safety therefore
// entirely relies on the user. Put and get operations must be explicitly
// serialized, otherwise put and get operations can occur in undefined order
// and results are undefined.
//
///////////////////////////////////////////////////////////////////////////////

public class Hashtable {
  // Constructor
  public static create(): Hashtable;

  // Number of key/element pairs
  public size(): int;

  // Returns true if the table contains the elements
  public contains<E>(element: E): boolean;

  // Returns true if the table contains the key
  public containsKey<K>(key: K): boolean;

  // If the table contains the key, returns the associated elements, otherwise
  // atomically associates the element to the key and returns the element. The
  // second argument is only evaluated when the key is added to the table the
  // first time.
  public get<K, E>(key: K, element: E): E;

  // Same thing, but returns a boolean indicating if the key has been added to
  // the table.
  public check<K, E>(key: K, element: E): boolean;

  // Atomically associates the element to the key. This function is not
  // compatible with the single-assignment semantics of the language (it is a
  // pure side-effect) and should be used with great care. Whenever possible,
  // the "get()" function should be used instead.
  public put<K, E>(key: K, element: E): E;

  // Associate each key to its matching element
  public assoc<K, E>(n: int)(keys: K[n], elements: E[n]): ();
  
  // Returns the array of keys of the table
  public keys<K>(): K[size()];

  // Returns the elements of the table
  public elements<E>(): E[size()];

  // Display
  public static dynamic lbrace: String = "{";
  public static dynamic arrow: String = " -> ";
  public static dynamic separator: String = ", ";
  public static dynamic rbrace: String = "}";
  
  // Underlying native object
  table: native;
  getKey<K, E>(key: K): E;
}

///////////////////////////////////////////////////////////////////////////////
//
//                               Implementation
//
///////////////////////////////////////////////////////////////////////////////

Hashtable.create() =
  new Hashtable(table = native("java.util.Hashtable()"));

size@Hashtable() = native("int java.util.Hashtable.size()", table);

// TEMPORARY (SHOULD BE ATOMIC)
getKey@Hashtable(key) =
  native("java.lang.Object "
         "java.util.Hashtable.get(java.lang.Object)", table, key);

// TEMPORARY (SHOULD BE ATOMIC)
get@Hashtable(key, element) = (containsKey(key) ?
                               getKey(key) : (table'; element))
{
  table' = native("java.lang.Object "
                  "java.util.Hashtable.put(java.lang.Object,java.lang.Object)",
                  table, key, element);
}

// TEMPORARY (SHOULD BE ATOMIC)
check@Hashtable(key, element) = (containsKey(key) ? false : (put; true))
{
  put = native("java.lang.Object "
               "java.util.Hashtable.put(java.lang.Object,java.lang.Object)",
               table, key, element);
}

// TEMPORARY (SHOULD BE ATOMIC)
put@Hashtable(key, element) = (table'; element)
{
  table' = native("java.lang.Object "
                  "java.util.Hashtable.put(java.lang.Object,java.lang.Object)",
                  table, key, element);
}

contains@Hashtable(element) =
  native("boolean java.util.Hashtable.contains(java.lang.Object)",
         table, element);
  
containsKey@Hashtable(key) =
  native("boolean java.util.Hashtable.containsKey(java.lang.Object)",
         table, key);
  
keys@Hashtable() = elements
{
  enum = native("java.util.Enumeration "
                "java.util.Hashtable.keys()",
                table);
  fun next() = native("java.lang.Object "
                      "java.util.HashtableEnumerator.nextElement()",
                      enum);
  elements = [next(), i -> (elements[i-1]; next())];
}

elements@Hashtable() = elements
{
  enum = native("java.util.Enumeration "
                "java.util.Hashtable.elements()",
                table);
  fun next() = native("java.lang.Object "
                      "java.util.HashtableEnumerator.nextElement()",
                      enum);
  elements = [next(), i -> (elements[i-1]; next())];
}

toString@Hashtable() = format("%s%s%s",
                              lbrace,
                              size() == 0 ? "" : str[size() - 1],
                              rbrace)
{
  ks = keys();
  str = [format("%a%s%a", ks[0], arrow, getKey(ks[0])),
         i -> format("%s%s%a%s%a",
                     str[i-1], separator, ks[i], arrow, getKey(ks[i]))];
}

assoc@Hashtable(n)(keys, elements) = b[n]
{
  b = [(), i -> (b[i - 1]; put(keys[i-1], elements[i-1]); ())];
}