History log of /seL4-l4v-master/HOL4/src/portableML/Redblackmap.sml
Revision Date Author Comments
# 2ef0db2e 10-Jan-2019 immler <immler@in.tum.de>

Uref.uref -> Uref.new


# b4bc28b4 10-Jan-2019 immler <immler@in.tum.de>

introduce Uref for both polyml and mosml


# b1ca9521 10-Sep-2018 Fabian Immler <immler@in.tum.de>

make heavily allocated variables explicit as local program variables


# 6a81a039 21-May-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove TABs from src

Will also make selftest to check that they aren't introduced


# ada82ed2 14-Feb-2011 Ramana Kumar <ramana.kumar@gmail.com>

Extend Redblackmap with update and findKey operations

update allows you to set the value for a key to some function of its old
value without traversing the tree twice. findKey returns the inserted
key along with its value, which may be useful if the lookup key is
different but still EQUAL as a key.

Strictly speaking these are not extensions to the original code, since I
have taken the obvious code reuse opportunities. So now find and insert
might waste some cycles constructing and deconstructing options and
closures.


# f595df26 03-Nov-2010 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Function fromList added.


# 24b80f04 07-Oct-2010 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Added a function insertList.


# 5fc2bdeb 12-Nov-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Added a function isEmpty that returns true if its argument is the empty map,
and false otherwise.


# 4761143b 10-Aug-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!


# 06b4cee6 27-May-2009 Peter Homeier <palantir@trustworthytools.com>

In preparation for making the standard kernel build under Poly/ML, removed the dependency of src/0/Term.sml on the Moscow ML library Polyhash, replacing this with RedBlackMap.

The building of HOL appears to be faster with RedBlackMap.

Also revised RedBlackMap.sml, RedBlackSet.sml, and HolKernel.sml to eliminate some annoying warning messages.


# 0e40e3ec 07-Nov-2005 Ken Friis Larsen <ken@friislarsen.net>

Updated to the latest version of Ken's private copy


# 67274ad0 07-Oct-2003 Joe Hurd <joe@gilith.com>

Added a few newlines at end of files to suppress warnings from my
Mosml -> MLton preprocessor.


# c50d07a5 13-Dec-2002 Michael Norrish <Michael.Norrish@nicta.com.au>

Red-black implmentations of the Binarymap signature. Quite possibly
very buggy. Didn't seem to make a big efficiency difference in Term.compare so
I didn't test them extensively.