module AiPL-Lab where

open import AiPL-Lecture

{- I Vectors -}

{- Vectors are "lists indexed by their length". They're good for
enforcing length invariants on operations. (Sometimes it's good to ask
whether length invariants are important: vectors are not just the
drop-in replacement for lists in ordinary functional programming.) -}

      -- vvvvvvvvv the element type is abstracted over the whole definition
data Vec (X : Set) : Nat -> Set where
                  -- ^^^ the length index is not expected to be uniform
  [] : Vec X ze -- empty vectors have zero length
  _::_ : forall {n}(x : X)(xs : Vec X n) -> Vec X (su n)
         -- consing a head to a tail increases length by one;
         -- the length is an "implicit" argument

{- Try writing the function which takes the head of a vector. What's the
type of the function? One of these two will work out. -}

head0 : forall {X n} -> Vec X n -> X
head0 xs = {!!}

head : forall {X n} -> Vec X (su n) -> X
head xs = {!!}

tail : forall {X n} -> Vec X (su n) -> Vec X n
tail xs = {!!}

{- Write the function which makes a vector by coping a single value. -}

vec : forall {n X} -> X -> Vec X n
vec {n} x = {!!}

{- Curly braces in an application make a usually-implicit argument explicit.
Sometimes, inferable information is operationally relevant. As a result
arguments which can routinely be kept unseen at *usage* sites need to be
exposed at *definition* sites. -}

{- Write the function which takes a vector of functions and applies
them to a vector of arguments to produce a vector of results. Ensure
that the jth output is the result of applying the jth function to the
jth argument. -}

vapp : forall {n S T} -> Vec (S -> T) n -> Vec S n -> Vec T n
vapp fs ss = {!!}

{- Now use vec and vapp to implement the following. -}

vmap : forall {n S T} -> (S -> T) -> Vec S n -> Vec T n
vmap f ss = {!!}

vzip : forall {n S T} -> Vec S n -> Vec T n -> Vec (S * T) n
vzip ss ts = {!!}  -- you can refer to the pairing constructor as _,_

vtranspose : forall {m n X} -> Vec (Vec X n) m -> Vec (Vec X m) n
vtranspose xss = {!!}


{- II 2-3 Trees -}

{- 2-3 trees are trees which enforce uniform depth and hence
logarithmic access time. They must be kept balanced, but the
availability of nodes with *three* subtrees makes it easy to
amortize the cost of balancing. -}

data T23 (l u : Bnd Nat) : Nat -> Set where
  leaf0 : (l <B= u) -> T23 l u ze
  node2 : {n : Nat}(x : Nat) ->
    T23 l (val x) n -> T23 (val x) u n
    -> T23 l u (su n)
  node3 : {n : Nat}(x y : Nat) ->
    T23 l (val x) n -> T23 (val x) (val y) n -> T23 (val y) u n
    -> T23 l u (su n)

{- Implement insertion for 2-3 trees. You will need to use
"with" to do appropriate comparisons and to make recursive
calls. I've done the difficult bit, which is to write the
type. -}

insert23 : forall {n l u} ->  -- a height, some bounds
           Intv l u -> T23 l u n ->  -- a value, a tree, sharing bounds
             T23 l u n  -- either it fits, preserving the height
             +
             Sg Nat \ x -> T23 l (val x) n * T23 (val x) u n
               -- or it's *only slightly* too big, and we get the stuff
               -- for a node2 taller by one
insert23 (z , lz , zu) t = {!!}


{- III Simple Dependent Session Types -}

{- Let's have bits. -}

data Two : Set where tt ff : Two

[_/_] : {P : Two -> Set} -> P tt -> P ff -> (b : Two) -> P b
[ t / f ] tt = t
[ t / f ] ff = f

{- Let's define a collection of simple "signal" types. -}

data Signal : Set where
  !0 !1 !2 : Signal
  !Nat : Signal

Transmission : Signal -> Set
Transmission !0    = Zero
Transmission !1    = One
Transmission !2    = Two
Transmission !Nat  = Nat

{- Now, let's build a type of Protocols which consist of sending or
receiving simple signals, in turn. -}

data Protocol : Set
Trace : Protocol  -> Set

data Protocol where
  send : Signal -> Protocol         -- just send a signal
  op : Protocol -> Protocol         -- swap send and receive
  seq : (A : Protocol)              -- send according to A, then
        (B : Trace A -> Protocol)   -- depending on what happened,
        -> Protocol                 -- send according to B
{- The trace of a protocol is exactly the record of its signals. A later
protocol can depend on the *trace* of an earlier protocol. -}
Trace (send x)    = Transmission x
Trace (op P)      = Trace P
Trace (seq A B)   = Sg (Trace A) \ a -> Trace (B a)


{- Now define (by mutual recursion) what it is to be the sender or
receiver for a given protocol, with a given *goal*. That is,
   a Sender P G should send according to P, producing a trace satisfying G
   a Receiver P H should receive according P, so the trace satisfies H -}

Sender : (P : Protocol) -> (G : Trace P -> Set) -> Set
Receiver : (P : Protocol) -> (H : Trace P -> Set) -> Set

Sender P G = ?
Receiver P H = ?

{- You should then be able to define communication. Given a sender and a
receiver who agree on a protocol, produce the trace their interaction
generates and show that they both succeed in their goals! -}   

communicate : forall P {G H} -> Sender P G -> Receiver P H
  -> Sg (Trace P) \ p -> G p * H p
communicate P sg rh = ?

{- Define the session type binary connectives for protocols -}

_+P_ _*P_ _&P_ _>P_ : Protocol -> Protocol -> Protocol

A +P B = ?
A *P B = ?
A &P B = ?
A >P B = ?

{- A Binary Operation Server will
     - send a number m
     - send a number n
     - receive m bits
     - send n bits
     - stop

Construct the protocol for such a server.
Implement just such a server for your favourite components,
e.g. a full adder.
-}