Phone Book with Refinement Types Example
def module default {
  def entity User {
    id : Id,
    username : String,
    name : String,
    password : String,
    photo : String,
    phone : Int,
    creditCardNumber : String
  }
  read username, phone, name, password, photo
    where true
  read creditCardNumber
    where Authenticated(username)
  write username, phone, name, creditCardNumber, password, photo
    where Authenticated(username)
  
  def entity Photos {
    id : Id,
    username : String,
    photo : String,
    comment : String
  }
  read username where true
  read comment, photo where Authenticated(username)
  read comment, photo where (Friends(username, uid) and Authenticated(uid))
  write username, comment, photo where Authenticated(username)  
  
  def entity Friends {
    id : Id,
    username : String,
    friend : String
  }
  read username, friend where true
  write username, friend where Authenticated(username)
  invariant Friends(username, friend)

  def screen index {
    div title {
      label "Login"
    };
    br;
    label "Username: ";
    textfield username;
    br;
    label "Password: ";
    textfield password;
    label " ";
    button "Login" to login(username, password);
    br;
    br;
    link {
      label "Register"
    } to register()
  }

  def action login (uname: String, pwd: String): WebPage {
    if (authenticate(uname, pwd)) then 
        photosWall(uname)
    else 
        accessDenied()
  }

  def screen register {
    div title {
      label "Register"
    };
    br;
    label "Username: ";
    textfield username;
    br;
    label "Name: ";
    textfield name;
    br;
    label "Password: ";
    textfield password;
    br;
    label "Photo URL: ";
    textfield photo;
    br;
    label "Phone: ";
    textfield phone;
    br;
    label "Credit Card: ";
    textfield ccard;
    br;
    button "Create User" to newUser(username, name, password, photo, phone, ccard);
    br;
    br;
    link {
      label "Login"
    } to index()
  }
  
  def action authenticate (uname: String, pwd: String):
                                                {z: Bool | (z -> Authenticated(uname))} {
    let list =  from (x in User) 
      where ((x.username == uname) and (x.password == pwd)) 
      select {
        name = x.name
      } in (if (isNotEmpty(list)) then {
        assume Authenticated(uname);
        true
      } else 
        false)
  }
  
  def screen accessDenied {
    div title {
      label "Access Denied"
    };
    br;
    link {
      label "Back"
    } to index()
  }

  def screen photosWall (uname: {x: String | Authenticated(x)}) {
    div bottom {
      div right {
        link {
          label "Profile Settings"
        } to userProfile(uname)
      };
      div right {
        link {
          label "Logout"
        } to index()
      }
    };
    div title {
      label getUserName(uname);
      label "'s ";
      label "Photos Wall"
    };
    br;
    iterator (row in  from (y in Friends) 
      where (y.friend == uname) 
      select y) {
      label let username = row.username in (listFriendsPhotos(username, uname))
    }
  }  
  
  def action newUser (uname: String, nm: String, pwd: String, ph: String, phnr: String,
                                                                ccard: String): WebPage {
    assume Authenticated(uname);
    insert {
      username = uname,
      name = nm,
      password = pwd,
      photo = ph,
      phone = str2int(phnr),
      creditCardNumber = ccard
    } in User;
    index()
  }  
  
  def screen userProfile (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Logout"
      } to index()
    };
    br;
    div title {
      label "My Profile"
    };
    br;
    iterator (row in  from (x in User) 
      where (x.username == uname) 
      select x) {
      div photo {
        image row.photo
      };
      label ("Username: " + row.username);
      br;
      label ("Name: " + row.name);
      br;
      label ("Phone: " + row.phone);
      br;
      label ("Credit Card: " + row.creditCardNumber);
      div clear {
        br
      }
    };
    div square {
      div right {
        link {
          label "Grant Permission"
        } to addFriend(uname);
        label " (adds a friend)";
        label " "
      };
      link {
        label "Check Permisisons"
      } to friendsPermissions(uname);
      br;
      br;
      link {
        label "Add Photo"
      } to addPhoto(uname);
      br;
      link {
        label "My Photos"
      } to listMyPhotos(uname);
      br;
      link {
        label "My Friends"
      } to userFriends(uname);
      br;
      link {
        label "Edit"
      } to edit(uname);
      br;
      link {
        label "Phone Book"
      } to phoneBook(uname);
      br;
      link {
        label "Photos Wall"
      } to photosWall(uname);
      br
    };
    div clear {
      br
    }
  }  

  def action getUserName (uname: String): String {
        foreach p in ( from (x in User) 
      where (x.username == uname) 
      select {
        name = x.name
      }) do
      p.name
  }
  
  def screen listFriendsPhotos (user: {x: String |
                       (Friends(x, friend) and Authenticated(friend))}, friend: String) {
    iterator (row in  from (y in Photos) 
      where (user == y.username) 
      select {
        photo = y.photo,
        comment = y.comment
      }) {
      div photo {
        image getProfilePhoto(user);
        div bold {
          label getUserName(user)
        }
      };
      image row.photo;
      br;
      div h1 {
        label row.comment
      };
      br
    }
  }
  
  def screen addFriend (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Back to My Profile"
      } to userProfile(uname)
    };
    br;
    div title {
      label "Add Friend"
    };
    br;
    label "Friend: ";
    textfield friend;
    br;
    button "Grant Permission" to newFriend(uname, friend);
    br;
    br
  }
  
  def screen friendsPermissions (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Back to My Profile"
      } to userProfile(uname)
    };
    br;
    div title {
      label "Permissions"
    };
    br;
    iterator (row in  from (x in Friends) 
      where (x.username == uname) 
      select x) {
      label ("Name: " + getUserName(row.friend));
      br;
      image getFriendPhoto(row.friend);
      br;
      button "Revoke Permission" to removeFriend(uname, row.friend);
      br
    }
  }
  
  def screen addPhoto (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Back to My Profile"
      } to userProfile(uname)
    };
    br;
    div title {
      label "Add Photo"
    };
    br;
    label "Photo: ";
    textfield nphoto;
    br;
    label "Comment: ";
    textfield cm;
    br;
    button "Add Photo" to newPhoto(uname, nphoto, cm);
    br;
    br
  }
  
  def screen listMyPhotos (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Back to My Profile"
      } to userProfile(uname)
    };
    br;
    div title {
      label "My Photos"
    };
    br;
    iterator (row in  from (y in Photos) 
      where (uname == y.username) 
      select y) {
      image row.photo;
      button "Remove Photo" to removePhoto(uname, row.photo);
      br;
      div h1 {
        label ("Comment: " + row.comment)
      }
    }
  }
    
  def screen userFriends (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Back to My Profile"
      } to userProfile(uname)
    };
    br;
    div title {
      label "My Friends"
    };
    br;
    iterator (row in  from (x in Friends) 
      where (x.friend == uname) 
      select x) {
      label ("Name: " + getUserName(row.username));
      br;
      image getFriendPhoto(row.username);
      br
    }
  }
  
  def screen edit (uname: {x: String | Authenticated(x)}) {
    div title {
      label "My Profile"
    };
    br;
    iterator (row in  from (x in User) 
      where (x.username == uname) 
      select x) {
      div photo {
        image row.photo
      };
      label "Username: ";
      textfield username with row.username;
      br;
      label "Name: ";
      textfield name with row.name;
      br;
      label "Password: ";
      textfield password with row.password;
      br;
      label "Photo URL: ";
      textfield photo with row.photo;
      br;
      label "Phone: ";
      textfield phone with row.phone;
      br;
      label "CrediCard: ";
      textfield creditCard with row.creditCardNumber;
      br;
      button "Update User" to updateUser(uname, name, password, photo, phone, creditCard);
      button "Cancel" to userProfile(uname);
      br
    }
  }
  
  def screen phoneBook (uname: {x: String | Authenticated(x)}) {
    div square {
      link {
        label "Back to My Profile"
      } to userProfile(uname)
    };
    br;
    div title {
      label "Phone Book"
    };
    br;
    iterator (row in  from (y in User) 
      select {
        name = y.name,
        uname = y.username,
        phone = y.phone
      }) {
      div square {
        link {
          label row.name
        } to userDetails(uname, row.uname);
        label (("(Phone: " + row.phone) + ")");
        br
      };
      br;
      br
    }
  }
  
  def action getProfilePhoto (uname: String): String {
        foreach p in ( from (x in User) 
      where (x.username == uname) 
      select {
        ph = x.photo
      }) do
      p.ph
  }

  def action newFriend (uname: {x: String | Authenticated(x)}, fr: String): WebPage {
    let list =  from (x in User) 
      where (x.username == fr) 
      select {
        user = x.username
      } in (if (isNotEmpty(list)) then {
        assume Friends(uname, fr);
        insert {
          username = uname,
          friend = fr
        } in Friends;
        userProfile(uname)
      } else 
        noSuchUser(uname))
  }
  
  def action getFriendPhoto (uname: String): WebPage {
    foreach p in ( from (y in User) 
      where (y.username == uname) 
      select {
        ph = y.photo
      }) do
        p.ph
  }
  
  def action removeFriend (uname: {x: String | Authenticated(x)}, fr: String): WebPage {
    delete x from Friends where ((uname == x.username) and (fr == x.friend));
    friendsPermissions(uname)
  }
  
  def action removePhoto (uname: {x: String | Authenticated(x)}, photo: String): WebPage {
    delete x from Photos where ((uname == x.username) and (photo == x.photo));
    listMyPhotos(uname)
  }

  def action isFriendOf (uname: {x: String | Authenticated(x)}, fr: String):
                                                  {z: Bool | (z -> Friends(uname, fr))} {
    let vs =  from (f in Friends) 
      where ((f.username == uname) and (f.friend == fr)) 
      select f in (if (isNotEmpty(vs)) then {
        getHead(vs);
        true
      } else 
        false)
  }

  def screen noSuchUser (uname: {x: String | Authenticated(x)}) {
    div title {
      label "User does not exist!"
    };
    br;
    link {
      label "Back"
    } to addFriend(uname)
  }

  def action newPhoto (uname: {x: String | Authenticated(x)}, ph: String, cm: String):
                                                                                WebPage {
    insert {
      username = uname,
      photo = ph,
      comment = cm
    } in Photos;
    userProfile(uname)
  }

  def screen userDetails (logged: {x: String | Authenticated(x)}, uname: String) {
    link {
      label "Back to My Profile"
    } to userProfile(logged);
    label " ";
    link {
      label "Back to Phone Book"
    } to phoneBook(logged);
    div title {
      label ("User Details: " + uname)
    };
    br;
    iterator (row in  from (x in User) 
      where (x.username == uname) 
      select {
        uname = x.username,
        name = x.name,
        phone = x.phone
      }) {
      label ("Name: " + row.name);
      br;
      label ("Phone: " + row.phone)
    };
    br
  }

  def action updateUser (uname: {x: String | Authenticated(x)}, nm: String, pwd: String,
                                      ph: String, phnr: String, ccard: String): WebPage {
    update x in User with {
      username = uname,
      name = nm,
      password = pwd,
      phone = str2int(phnr),
      photo = ph,
      creditCardNumber = ccard
    } where (x.username == uname);
    userProfile(uname)
  }
}

Back