
\section{Application}

As an application, we propose to build a grade sheet in this programming language.

We are planning to use it for more complex applications such as a wiki,
but we will need to dynamically create ressources which is not yet
possible, we will discuss this point in the conclusion.

\subsection*{Example : grade sheet}

The policies we want to have in this application are very similar
to the ones in \ref{example}.

We have one database, lets call it $gradedb$.
Policies would be

%$$ p1 : Alice \, \textup{says} \, \textsc {maywt} ( gradedb , Alice ) $$
%$$ p2 : Alice \, \textup{says} \, \textsc {mayrd} ( gradedb , Alice ) $$

$$ p1 : \textsc {maywt} ( gradedb , Alice ) $$
$$ p2 : \textsc {mayrd} ( gradedb , Alice ) $$

if $Alice$ is the teacher and for each student we will need to add a proposition of the form
%$$ p : Alice \, \textup{says} \, \textsc {mayrd} ( gradedb , Bob ) $$
$$ \textsc {mayrd} ( gradedb , Bob ) $$

The first thing we need is the user to login so that we have a 
value of type $identity$. 
This may redirect the user to a login server where he would have
to enter his login and password.

We then try to acquire certificates saying that we may read
and write the database.
If we have both then we are the teacher and we can edit the sheet,
if we only have read permissions then we can just display the grades.

\begin{verbatim}
extern database gradedb
principal user

val cookie = webiso ()
val id = checksig {user} cookie
val gradehandle = gethandle {gradedb} ()

val _ = match (id,gradehandle) with
   (SOME id, SOME gradehandle) =>
       acquire_cert{mayrd gradedb user}
       then p1 .
           acquire_cert{maywt gradedb user}
             then p2 . edit {user,gradedb,p1,p2,id,gradehandle} ()
             else display {user,gradedb,p1,id,gradehandle} ()
       else ()
   | _ => ()
     
\end{verbatim}

$\textup{edit}$ and $\textup{display}$ would be two functions
that I will not detail. 
Their types are 
\begin{verbatim}
val (u:principal,db:database,
     p1:TRUE mayrd db u, p2:TRUE maywt db u,
     id: u identity, h: db handle) edit : unit -> unit
val (u:principal,db:database,
     p1:TRUE mayrd db u,
     id: u identity, h: db handle) display : unit -> unit
\end{verbatim}

And in these functions a call to $\textup{read}$ will for
instance be performed like this 
\begin{verbatim}
val grades = read {db,u,p1} h id
\end{verbatim}



