(** Homework Assignment 7#<br>#
#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
Proving#</a><br>#
CS294-9, Fall 2006#<br>#
UC Berkeley *)

Require Import List.

Set Implicit Arguments.


(** This assignment involves producing two strongly-specified implementations of
  the same abstract data type.  We'll use Coq's module system to express this
  idea.  I don't think you need to be an expert on ML-style module systems to do
  this assignment, since I've filled in all of the module-related parts in the
  template, but the curious can consult
  #<a href="http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html">#the
  OCaml manual's tutorial#</a>#.

  Feel free to copy some of the infrastructure for programming with
  specifications from the #<a href="../lectures/lecture8.v">#Lecture 8
  code#</a>#; you might want to add some of your own code in that spirit, too.

  #<a href="HW7.v">#Template source file#</a>#
  *)


(** * Signatures *)

(** First, we define what it means to implement the dictionary ADT. *)
Module Type DICTIONARY.
  (** We have some [Set] that forms the keys of dictionaries. *)
  Parameter domain : Set.

  (** We have the type of dictionaries, indexed by the type of data being
    stored.
    *)
  Parameter dict : Set -> Set.

  (** Look up the data associated with a given key. *)
  Parameter lookup : forall (range : Set), dict range -> domain -> option range.

  (** The empty dictionary *)
  Parameter empty : forall (range : Set),
    {D : dict range | forall (d : domain), lookup D d = None}.

  (** Adding a mapping *)
  Parameter add : forall (range : Set) (D : dict range) (d : domain) (r : range),
    {D' : dict range | lookup D' d = Some r
      /\ forall (d' : domain), d <> d' -> lookup D' d' = lookup D d'}.
End DICTIONARY.

(** This signature defines what we will require from clients who want to build
  dictionaries for particular key types.
  *)
Module Type DICTIONARY_PARAM.
  Parameter domain : Set.
  Parameter domain_eq_dec : forall (x y : domain), {x = y} + {x <> y}.
  (** ...so all that we require is that equality on the key type is
    decidable.
    *)
End DICTIONARY_PARAM.


(** * Naive dictionaries using functions *)

(** We'll implement the dictionary ADT using the most obvious (and quite
  inefficient!) representation: dictionaries will be the lookup functions
  themselves.
  *)
Module FuncDictionary (Param : DICTIONARY_PARAM) : DICTIONARY
  with Definition domain := Param.domain.
  Import Param.

  Section dict.
    Variable range : Set.

    (** Defined as promised, dictionaries are lookup functions. *)
    Definition dict := domain -> option range.

    (** That makes [lookup] very convenient to write. [:-)] *)
    Definition lookup : dict -> domain -> option range := fun D => D.

    (** Fill in a definition for [empty]. *)
    Definition empty : {D : dict | forall (d : domain), lookup D d = None}.
    Admitted.

    (** Fill in a definition for [add]. *)
    Definition add : forall (D : dict) (d : domain) (r : range),
      {D' : dict | lookup D' d = Some r
	/\ forall (d' : domain), d <> d' -> lookup D' d' = lookup D d'}.
    Admitted.
  End dict.

  Definition domain := domain.
End FuncDictionary.

(** Of course, it's always fun to see the OCaml version of your
  implementation.
  *)
Extraction FuncDictionary.


(** * Dictionaries using unsorted lists *)

(** Now we'll implement dictionaries using the more efficient representation of
  unsorted association lists with no duplicates.
  *)
Module ListDictionary (Param : DICTIONARY_PARAM) : DICTIONARY
  with Definition domain := Param.domain.
  Import Param.

  Section dict.
    Variable range : Set.

    (** We start by defining an auxiliary dependent, list-like type.
      The list parameter to [dict'] expresses the keys that have "already been
      used" and so may not appear again.
      *)
    Inductive dict' : list domain -> Set :=
      | Nil : forall ls,
	dict' ls
      | Cons : forall ls d,
	~In d ls
	-> range
	-> dict' (d :: ls)
	-> dict' ls.

    (** A dictionary is just a [dict'] where no keys have already been used. *)
    Definition dict := dict' nil.

    (** The obvious lookup function *)
    Fixpoint lookup' (ls : list domain) (D : dict' ls) (d : domain) {struct D}
      : option range :=
      match D with
	| Nil _ => None
	| Cons _ d' _ r D' =>
	  if domain_eq_dec d d'
	    then Some r
	    else lookup' D' d
      end.

    Definition lookup := lookup' (ls := nil).

    (** Fill in a definition for [empty]. *)
    Definition empty : {D : dict | forall (d : domain), lookup D d = None}.
    Admitted.

    (** Fill in a definition for [add].  You'll probably want some auxiliary
      definitions for this one. *)
    Definition add : forall (D : dict) (d : domain) (r : range),
      {D' : dict | lookup D' d = Some r
	/\ forall (d' : domain), d <> d' -> lookup D' d' = lookup D d'}.
    Admitted.
  End dict.

  Definition domain := domain.
End ListDictionary.

Extraction ListDictionary.