(* You will need the modular implicits OCaml fork for this exercise

     opam switch 4.02.0+modular-implicits
*)

(* Preliminaries: APPLICATIVE and MELDABLE *)
module type APPLICATIVE =
sig
  type _ t
  val pure : 'a -> 'a t
  val (<*>) : ('a -> 'b) t -> 'a t -> 'b t
  (* Applicative laws
             pure h ⊗ pure v  ≡  pure (h v)
                 pure id ⊗ x  ≡  x
        pure (∘) ⊗ f ⊗ g ⊗ x  ≡  f ⊗ (g ⊗ x)
           pure (λf.f v) ⊗ g  ≡  g ⊗ pure v
  *)
end
module type MELDABLE =
sig
  type _ t
  val pure : 'a -> 'a t
  val meld : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
end

(* Preliminaries: the TRIE signature *)
module type TRIE =
sig
  type k
  type _ trie
  val all : 'v -> 'v trie
  val mix : ('a -> 'b -> 'c) -> 'a trie -> 'b trie -> 'c trie

  val set : k -> 'v -> 'v trie -> 'v trie
  val get : k -> 'v trie -> 'v
end

(* Preliminaries: overloaded functions, parameterized by an implicit
   module T of type TRIE *)
let all {T:TRIE} v = T.all v
let mix {T:TRIE} f l r = T.mix f l r
let set {T:TRIE} k v t = T.set k v t
let get {T:TRIE} k t = T.get k t

(* Preliminaries: the map and set signatures *)
module type SET = sig
  type t
  type elem

  (* Create an empty set *)
  val create : unit -> t

  (* Whether a set contains a particular element *)
  val member : elem -> t -> bool

  (* The union of two sets *)
  val mingle : t -> t -> t

  (* Add an element to a set *)
  val insert : elem -> t -> t

  (* Remove an element from a set *)
  val remove : elem -> t -> t
end

module type MAP = sig
  type 'v t
  type key

  (* Create an empty map *)
  val make : unit -> 'v t

  (* Retrieve the value corresponding to a key in a map *)
  val seek : key -> 'v t -> 'v option

  (* Join two maps together, using the function to merge values *)
  val join : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t

  (* Add a key to a map *)
  val push : key -> 'v -> 'v t -> 'v t

  (* Remove a key from a map *)
  val oust : key -> 'v t -> 'v t
end

(* Preliminaries: binary sums. *)
type ('a, 'b) sum =
    L : 'a -> ('a,'b) sum
  | R : 'b -> ('a,'b) sum

(* Preliminaries: natural numbers *)
type nat = Z : nat | S : nat -> nat

(* Preliminaries: INJ is a signature of injections from a type t into
   a type s. *)
module type INJ = sig
  type t and s

  (** Convert a t into an s *)
  val inj : t -> s
end

(* Preliminaries: the Empty exception *)
exception Empty

(* Preliminaries: the z and s constructors *)
type z = Z and _ s = S

(* Question 1(a): define Applicative_of_meldable
                     and Meldable_of_applicative *)
(*
module Applicative_of_meldable(M: MELDABLE) :
  APPLICATIVE with type 'a t = 'a M.t = [ANSWER]
module Meldable_of_applicative(A: APPLICATIVE) :
  MELDABLE with type 'a t = 'a A.t = [ANSWER]
*)

(* Question 1(b): complete the equivalence proof by giving laws for Meldable
   and showing that the Applicative laws follow from the Meldable laws and
   vice versa

    [ANSWER]
*)

(* Question 2(a)(i): define Trie_unit, Trie_product and Trie_sum *)

(*
implicit module Trie_unit :
  TRIE with type k = unit and type 'v trie = ? [ANSWER]
 = ? [ANSWER]
*)


(*
module Trie_product (A: TRIE) (B: TRIE)
  : TRIE with type k = A.k * B.k and type 'v trie = ? [ANSWER] =
 = ? [ANSWER]
*)

(*
module Trie_sum (A: TRIE) (B: TRIE)
 : TRIE with type k = (A.k, B.k) sum
        and type 'v trie = ? [ANSWER]
  = ? [ANSWER]
*)

(* Question 2(a)(ii): define Trie_iso, Trie_bool and Trie_option *)

(*
module Trie_iso (A: TRIE) (S: INJ with type s = A.k) :
  TRIE with type k = S.t and type 'v trie = 'v A.trie =
  ? [ANSWER]
*)

(*
  implicit module Trie_bool : TRIE with type k = bool
                                    and type 'v trie = ? [ANSWER]
  = ? [ANSWER]
*)

(*
  implicit module Trie_option (A: TRIE) :
    TRIE with type k = A.k option
          and type 'v trie = ? [ANSWER]
    = ? [ANSWER]
*)


(* Question 2(a)(iii): define Trie_default, Trie_nat and Trie_list *)

type ('p, 'a) default = Present : 'p -> ('p, 'a) default
                      | Absent  : 'a -> ('p, 'a) default
(*
module Trie_default (A: TRIE) :
  TRIE with type k = A.k
  with type 'v trie = ('v A.trie, 'v) default =
struct
  type k = A.k
  type 'v trie = ('v A.trie, 'v) default

  let all v = Absent v

  [ANSWER]
*)

(* (Uncomment Trie_fix when Trie_default is defined) *) 
(*
module Trie_fix (F:(functor (X: TRIE) -> TRIE)) =
struct
  module rec Fixed : sig
    type k = K : (F(Trie_default(Fixed)).k) -> k
    type 'v trie =  'v F(Trie_default(Fixed)).trie
    include TRIE with type k := k and type 'v trie := 'v trie
  end = 
    struct
      module X = F(Trie_default(Fixed))
      type k = K : (F(Trie_default(Fixed)).k) -> k
      type 'a trie = 'a X.trie
      let get (K x) t = X.get x t
      let set (K x) v t = X.set x v t
      let all x = X.all x
      let mix f l r = X.mix f l r
    end
end
*)


(*
implicit module Trie_nat
  : TRIE with type k = nat and type 'v trie = ? [ANSWER]
 = ? [ANSWER]
*)

(*
implicit module Trie_list {A: TRIE}
  : TRIE with type k = A.t list and type 'v trie = ? [ANSWER]
 = ? [ANSWER]
*)


(* Question 2(b): define MAP and SET implementations based on TRIE *)

(*
implicit module Set{T:TRIE}
  : SET with type elem = T.k = [ANSWER]
*)

(*
implicit module Map{T:TRIE}
  : MAP with type key = T.k = [ANSWER]
*)

(* Question 3(a): define sub using the two subtraction facts:
     n - n = 0
     if   m - n = o   then (m+1) - n = (o+1)
*)
type (_, _, _) sub (* = [ANSWER]
    SubZ : (?, ?, ?) sub
  | SubS : (?, ?, ?) sub -> (?, ?, ?) sub
*)

(* Question 3(b): define subsuc, a proof of the following fact:
    if   m - n = o    then   (1+m) - (1+n) = o
*)
(* let rec subsuc [ANSWER] *)

(* Question 3(c): define vectors with nil, cons and length.

  (You may change the stub definitions, e.g. changing 'let' to 'let rec'
   if necessary, so long as the types remain the same and the behaviour
   is correct.)
 *)
type (+'a,'n) vec (* = [ANSWER] *)
(* let length : 'a 'n.('a, 'n) vec -> ('n, z, 'n) sub = [ANSWER]  *)
(* let nil : 'a. ('a, z) vec = [ANSWER] *)
(* let cons : 'a. 'a -> ('a, 'n) vec -> ('a, 'n s) vec = [ANSWER] *)

(* Question 3(d): define rev_append and revappend_result *)
type ('a, 'm, 'n) revappend_result (* = [ANSWER] *)

(* let rec rev_append : type a m n o. (a, m) vec -> (a, n) vec ->
     (a, m, n) revappend_result = [ANSWER] *)

(* Question 3(e): define queues using vec and sub *)
type 'a queue = Q : ('a, 'lenf) vec * (* f *)
                    ('a, 'lenr) vec * (* r *)
                    ('lenf, 'lenr, _) sub ->
  'a queue

(* let isEmpty : 'a. 'a queue -> bool = [ANSWER] *)
(* let enq : 'a. 'a -> 'a queue -> 'a queue = [ANSWER] *)
(* let deq : 'a. 'a queue -> 'a * 'a queue = [ANSWER] *)

(*  
 * Finally, it would be helpful to know how long you spent on this
 * exercise.  There is no obligation to answer this question if you would
 * prefer not to!  I plan to use the information provided to improve the
 * course, and will not distribute the information further except possibly
 * in anonymised form.  (E.g. I would like to produce and perhaps share
 * aggregate statistics such as the range, median, variance, etc., but
 * will not identify any individual student.)
 * 
 * How many hours did you spend on this exercise?
 *    [ANSWER]
 *)