type user = int
table user : { Id : user, Nam : string, Pass : string }
  PRIMARY KEY Id

task initialize = fn () =>
    b <- nonempty user;
    if b then
        return ()
    else
        dml (INSERT INTO user (Id, Nam, Pass)
             VALUES (0, 'a', 'a'));
        dml (INSERT INTO user (Id, Nam, Pass)
             VALUES (1, 'b', 'b'))

policy sendClient (SELECT *
                   FROM user
                   WHERE known(user.Pass))

type secret = int
sequence secretIds
table secret : { Id : secret, User : user, Nam : string, Value : string }
  PRIMARY KEY Id,
  CONSTRAINT User FOREIGN KEY User REFERENCES user(Id) ON DELETE CASCADE

policy sendClient (SELECT *
                   FROM secret, user
                   WHERE secret.User = user.Id
                     AND known(user.Pass))

policy mayInsert (SELECT *
                  FROM secret AS New, user
                  WHERE New.User = user.Id
                    AND known(user.Pass)
                    AND known(New.Nam)
                    AND known(New.Value))

policy mayDelete (SELECT *
                  FROM secret AS Old, user
                  WHERE Old.User = user.Id
                    AND known(user.Pass))

policy mayUpdate (SELECT *
                  FROM secret AS Old, secret AS New, user
                  WHERE Old.User = user.Id
                    AND known(user.Pass)
                    AND known(New.Value)
                    AND New.Id = Old.Id
                    AND New.User = Old.User)

cookie login : { Id : user, Pass : string }

fun isOk r = oneRowE1 (SELECT COUNT( * ) > 0
                       FROM user
                       WHERE user.Id = {[r.Id]}
                         AND user.Pass = {[r.Pass]})

fun userId () =
    ro <- getCookie login;
    case ro of
        None => return None
      | Some r =>
        b <- isOk r;
        return (if b then
                    Some r.Id
                else
                    None)

fun viewSecret id =
    let
        fun save r =
            u <- userId ();
            case u of
                None => error <xml>You're not logged in, so you can't modify secrets!</xml>
              | Some u =>
                dml (UPDATE secret
                     SET Value = {[r.Value]}
                     WHERE Id = {[id]}
                       AND User = {[u]});
                viewSecret id
    in
        u <- userId ();

        x <- (case u of
                  None => return <xml>You're not logged in, so you can't view secrets!</xml>
                | Some u =>
                  queryX1 (SELECT secret.Nam, secret.Value
                           FROM secret
                           WHERE secret.Id = {[id]}
                             AND secret.User = {[u]})
                          (fn r => <xml>
                            <h2>{[r.Nam]}</h2>

                            <p>{[r.Value]}</p>
                          </xml>));

        return <xml>
          <head><title>The Secret</title></head>

          <body>
            {x}
            
            <hr/>

            <h3>Set a new value</h3>

            <form>
              <textbox{#Value}/> <submit value="Set" action={save}/>
            </form>
          </body>
        </xml>
    end

fun main () =
    u <- userId ();

    ss <- (case u of
               None => return <xml/>
             | Some u => queryX1 (SELECT secret.Id, secret.Nam
                                  FROM secret
                                  WHERE secret.User = {[u]})
                         (fn r => <xml><li><a link={viewSecret r.Id}>{[r.Nam]}</a>
                           <form> <submit action={delete r.Id} value="Delete"/> </form></li></xml>));

    return <xml>
      <head><title>Secret Keeper</title></head>

      <body>
        {case u of
             None => <xml>
               <h2>Log in</h2>

               <form><table>
                 <tr> <th>Name:</th> <td><textbox{#Nam}/></td> </tr>
                 <tr> <th>Password:</th> <td><password{#Pass}/></td> </tr>
                 <tr> <td><submit action={logon}/></td> </tr>
               </table></form>
             </xml>
           | Some u => <xml>
             <h3>Welcome, #{[u]}!</h3>
             
             <form>
               <submit value="Log off" action={logoff}/>
             </form>

             <hr/>

             <h3>New Secret</h3>

             <form><table>
                 <tr> <th>Name:</th> <td><textbox{#Nam}/></td> </tr>
                 <tr> <th>Value:</th> <td><textbox{#Value}/></td> </tr>
                 <tr> <td><submit action={add}/></td> </tr>
               </table></form>

             <hr/>

             {ss}
           </xml>}
      </body>
    </xml>

and logon r =
    ro <- oneOrNoRows (SELECT user.Id
                       FROM user
                       WHERE user.Nam = {[r.Nam]}
                         AND user.Pass = {[r.Pass]});
    case ro of
        None => error <xml>Wrong username or password!</xml>
      | Some r' =>
        setCookie login {Value = {Id = r'.User.Id, Pass = r.Pass}, Secure = False, Expires = None};
        main ()

and logoff () =
    clearCookie login;
    main ()

and add r =
    u <- userId ();
    case u of
        None => error <xml>You can't add a secret when you aren't logged in!</xml>
      | Some u =>
        id <- nextval secretIds;
        dml (INSERT INTO secret (Id, User, Nam, Value)
             VALUES ({[id]}, {[u]}, {[r.Nam]}, {[r.Value]}));
        main ()

and delete id () =
    u <- userId ();
    case u of
        None => error <xml>You can't delete a secret when you aren't logged in!</xml>
      | Some u =>
        dml (DELETE FROM secret
             WHERE User = {[u]}
               AND Id = {[id]});
        main ()