#
6fa7478f |
|
28-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Lift Table functor out of fromIsabelle into src/portableML This code is Isabelle's workhorse version of our Binarymap. It has a better API for working with maps into lists of values, and is also better in that its use of a functor means that the types of maps/dictionaries/tables using different comparison functions are different. I have altered it to use HOL style comparison functions that are curried rather than tupled. (I.e., in Isabelle the equivalents of our various op_<operation> functions are take a comparison function that takes a pair of arguments; our tradition is to use a curried function.) I have also added pretty-printing, requiring KEY-structures to provide a pp function. (These functions ignore depth arguments for the moment.) Finally, there are a number of knock-on effects in the fromIsabelle directory.
|