src/Tools/Metis/src/KeyMap.sml

fixed paths in Nitpick's ML file headers

(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)

functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
struct

(*isabelle open Metis;*)

type key = Key.t;

(* ------------------------------------------------------------------------- *)
(* Finite maps                                                               *)
(* ------------------------------------------------------------------------- *)

type 'a map = (Key.t,'a) Map.map;

fun new () = Map.new Key.compare;

val null = Map.null;

val size = Map.size;

fun singleton key_value = Map.singleton Key.compare key_value;

val inDomain = Map.inDomain;

val peek = Map.peek;

val insert = Map.insert;

val insertList = Map.insertList;

val get = Map.get;

(* Both union and intersect prefer keys in the second map *)

val union = Map.union;

val intersect = Map.intersect;

val delete = Map.delete;

val difference = Map.difference;

val subsetDomain = Map.subsetDomain;

val equalDomain = Map.equalDomain;

val mapPartial = Map.mapPartial;

val filter = Map.filter;

val map = Map.map;

val app = Map.app;

val transform = Map.transform;

val foldl = Map.foldl;

val foldr = Map.foldr;

val findl = Map.findl;

val findr = Map.findr;

val firstl = Map.firstl;

val firstr = Map.firstr;

val exists = Map.exists;

val all = Map.all;

val domain = Map.domain;

val toList = Map.toList;

fun fromList l = Map.fromList Key.compare l;

val compare = Map.compare;

val equal = Map.equal;

val random = Map.random;

val toString = Map.toString;

(* ------------------------------------------------------------------------- *)
(* Iterators over maps                                                       *)
(* ------------------------------------------------------------------------- *)

type 'a iterator = (Key.t,'a) Map.iterator;

val mkIterator = Map.mkIterator;

val mkRevIterator = Map.mkRevIterator;

val readIterator = Map.readIterator;

val advanceIterator = Map.advanceIterator;

end

(*isabelle structure Metis = struct open Metis*)

structure IntMap =
KeyMap (IntOrdered);

structure StringMap =
KeyMap (StringOrdered);

(*isabelle end;*)