(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

(** * Finite map library *)  

(** This file proposes interfaces for finite maps *)

Require Export Bool DecidableType OrderedType.
Set Implicit Arguments.
Unset Strict Implicit.

(** When compared with Ocaml Map, this signature has been split in 
    several parts : 

   - The first parts [WSfun] and [WS] propose signatures for weak
     maps, which are maps with no ordering on the key type nor the
     data type.  [WSfun] and [WS] are almost identical, apart from the
     fact that [WSfun] is expressed in a functorial way whereas [WS]
     is self-contained. For obtaining an instance of such signatures,
     a decidable equality on keys in enough (see for example
     [FMapWeakList]). These signatures contain the usual operators
     (add, find, ...). The only function that asks for more is
     [equal], whose first argument should be a comparison on data.

   - Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the 
     case where the key type is ordered. The main novelty is that 
     [elements] is required to produce sorted lists.

   - Finally, [Sord] extends [S] with a complete comparison function. For 
     that, the data type should have a decidable total ordering as well. 

   If unsure, what you're looking for is probably [S]: apart from [Sord],
   all other signatures are subsets of [S]. 

   Some additional differences with Ocaml: 
    
    - no [iter] function, useless since Coq is purely functional
    - [option] types are used instead of [Not_found] exceptions
    - more functions are provided: [elements] and [cardinal] and [map2]

*)



(** ** Weak signature for maps
   
    No requirements for an ordering on keys nor elements, only decidability
    of equality on keys. First, a functorial signature: *)

Module Type WSfun (E : EqualityType).

  (** The module E of base objects is meant to be a [DecidableType]
     (and used to be so). But requiring only an [EqualityType] here
     allows subtyping between weak and ordered maps. *)

  Definition key := E.t.

  Parameter t : Set -> Set. 
  (** the abstract type of maps *)
 
  Section Types. 

    Variable elt:Set.

    Parameter empty : t elt.
    (** The empty map. *)

    Parameter is_empty : t elt -> bool.
    (** Test whether a map is empty or not. *)

    Parameter add : key -> elt -> t elt -> t elt.
    (** [add x y m] returns a map containing the same bindings as [m], 
	plus a binding of [x] to [y]. If [x] was already bound in [m], 
	its previous binding disappears. *)

    Parameter find : key -> t elt -> option elt. 
    (** [find x m] returns the current binding of [x] in [m], 
	or [None] if no such binding exists. *)

    Parameter remove : key -> t elt -> t elt.
    (** [remove x m] returns a map containing the same bindings as [m], 
	except for [x] which is unbound in the returned map. *)

    Parameter mem : key -> t elt -> bool.
    (** [mem x m] returns [true] if [m] contains a binding for [x], 
	and [false] otherwise. *)

    Variable elt' : Set. 
    Variable elt'': Set.

    Parameter map : (elt -> elt') -> t elt -> t elt'.
    (** [map f m] returns a map with same domain as [m], where the associated 
	value a of all bindings of [m] has been replaced by the result of the
	application of [f] to [a]. Since Coq is purely functional, the order
        in which the bindings are passed to [f] is irrelevant. *)

    Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
    (** Same as [map], but the function receives as arguments both the 
	key and the associated value for each binding of the map. *)

    Parameter map2 : 
     (option elt -> option elt' -> option elt'') -> t elt -> t elt' ->  t elt''.
    (** [map2 f m m'] creates a new map whose bindings belong to the ones 
        of either [m] or [m']. The presence and value for a key [k] is 
        determined by [f e e'] where [e] and [e'] are the (optional) bindings 
        of [k] in [m] and [m']. *)

    Parameter elements : t elt -> list (key*elt).
    (** [elements m] returns an assoc list corresponding to the bindings 
        of [m], in any order. *)

    Parameter cardinal : t elt -> nat. 
    (** [cardinal m] returns the number of bindings in [m]. *)

    Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
    (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], 
	where [k1] ... [kN] are the keys of all bindings in [m] 
	(in any order), and [d1] ... [dN] are the associated data. *)

    Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
    (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal, 
      that is, contain equal keys and associate them with equal data. 
      [cmp] is the equality predicate used to compare the data associated 
      with the keys. *)

    Section Spec. 
      
      Variable m m' m'' : t elt.
      Variable x y z : key.
      Variable e e' : elt.

      Parameter MapsTo : key -> elt -> t elt -> Prop.

      Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.

      Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.

      Definition eq_key (p p':key*elt) := E.eq (fst p) (fst p').
      
      Definition eq_key_elt (p p':key*elt) := 
          E.eq (fst p) (fst p') /\ (snd p) = (snd p').

    (** Specification of [MapsTo] *)
      Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
      
    (** Specification of [mem] *)
      Parameter mem_1 : In x m -> mem x m = true.
      Parameter mem_2 : mem x m = true -> In x m. 
      
    (** Specification of [empty] *)
      Parameter empty_1 : Empty empty.

    (** Specification of [is_empty] *)
      Parameter is_empty_1 : Empty m -> is_empty m = true. 
      Parameter is_empty_2 : is_empty m = true -> Empty m.
      
    (** Specification of [add] *)
      Parameter add_1 : E.eq x y -> MapsTo y e (add x e m).
      Parameter add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
      Parameter add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.

    (** Specification of [remove] *)
      Parameter remove_1 : E.eq x y -> ~ In y (remove x m).
      Parameter remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
      Parameter remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.

    (** Specification of [find] *)
      Parameter find_1 : MapsTo x e m -> find x m = Some e. 
      Parameter find_2 : find x m = Some e -> MapsTo x e m.

    (** Specification of [elements] *)
      Parameter elements_1 : 
        MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
      Parameter elements_2 : 
        InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
      (** When compared with ordered maps, here comes the only 
         property that is really weaker: *)
      Parameter elements_3w : NoDupA eq_key (elements m).  

    (** Specification of [cardinal] *)
      Parameter cardinal_1 : cardinal m = length (elements m).

    (** Specification of [fold] *)  
      Parameter fold_1 :
	forall (A : Type) (i : A) (f : key -> elt -> A -> A),
        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 
   Definition Equal cmp m m' := 
         (forall k, In k m <-> In k m') /\ 
         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  

   Variable cmp : elt -> elt -> bool. 

   (** Specification of [equal] *)
     Parameter equal_1 : Equal cmp m m' -> equal cmp m m' = true. 
     Parameter equal_2 : equal cmp m m' = true -> Equal cmp m m'.

    End Spec. 
   End Types. 

    (** Specification of [map] *)
      Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
        MapsTo x e m -> MapsTo x (f e) (map f m).
      Parameter map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), 
        In x (map f m) -> In x m.
 
    (** Specification of [mapi] *)
      Parameter mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)
        (f:key->elt->elt'), MapsTo x e m -> 
        exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
      Parameter mapi_2 : forall (elt elt':Set)(m: t elt)(x:key)
        (f:key->elt->elt'), In x (mapi f m) -> In x m.

    (** Specification of [map2] *)
      Parameter map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
	(x:key)(f:option elt->option elt'->option elt''), 
	In x m \/ In x m' -> 
        find x (map2 f m m') = f (find x m) (find x m').       

     Parameter map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
	(x:key)(f:option elt->option elt'->option elt''), 
        In x (map2 f m m') -> In x m \/ In x m'.

  Hint Immediate MapsTo_1 mem_2 is_empty_2
    map_2 mapi_2 add_3 remove_3 find_2
    : map.
  Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
    remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
    : map.

End WSfun.


(** ** Static signature for Weak Maps 

    Similar to [WSfun] but expressed in a self-contained way. *)

Module Type WS. 
  Declare Module E : EqualityType.
  Include Type WSfun E.
End WS.



(** ** Maps on ordered keys, functorial signature *)

Module Type Sfun (E : OrderedType).
  Include Type WSfun E.
  Section elt.
  Variable elt:Set.
   Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
   (* Additional specification of [elements] *)
   Parameter elements_3 : forall m, sort lt_key (elements m).
   (** Remark: since [fold] is specified via [elements], this stronger
   specification of [elements] has an indirect impact on [fold],
   which can now be proved to receive elements in increasing order. *) 
  End elt.
End Sfun.



(** ** Maps on ordered keys, self-contained signature *)

Module Type S. 
  Declare Module E : OrderedType.
  Include Type Sfun E.
End S.



(** ** Maps with ordering both on keys and datas *)

Module Type Sord.

  Declare Module Data : OrderedType.   
  Declare Module MapS : S. 
  Import MapS.
  
  Definition t := MapS.t Data.t. 

  Parameter eq : t -> t -> Prop.
  Parameter lt : t -> t -> Prop. 
 
  Axiom eq_refl : forall m : t, eq m m.
  Axiom eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
  Axiom eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
  Axiom lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
  Axiom lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.

  Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end.	

  Parameter eq_1 : forall m m', Equal cmp m m' -> eq m m'.
  Parameter eq_2 : forall m m', eq m m' -> Equal cmp m m'.

  Parameter compare : forall m1 m2, Compare lt eq m1 m2.
  (** Total ordering between maps. [Data.compare] is a total ordering 
      used to compare data associated with equal keys in the two maps. *)

End Sord.