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 screen index {
    div title {
      label "Login"
    };
    label "Username: ";
    textfield username;
    br;
    label "Passowrd: ";
    textfield password;
    button "Login" to login(username, password);
    br;
    link {
      label "Register"
    } to register()
  }

  def action login (uname: String, pwd: String): WebPage {
    let x = authenticate(uname, pwd) in (userProfile(x))
  }

  def screen register {
    div title {
      label "Register"
    };
    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)
  }

  def action authenticate (uname: String, pwd: String): {z: String | Authenticated(z)} {
    let c = count( from (x in User) 
      where ((x.username == uname) and (x.password == pwd)) 
      select {
        name = x.name
      }) in (let w = assume Authenticated(uname) in (uname))
  }

  def screen userProfile (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: " + row.username);
      br;
      label ("Name: " + row.name);
      br;
      label ("Phone: " + row.phone);
      br;
      label ("Credit Card: " + row.creditCardNumber)
    };
    br;
    br;
    div square {
      link {
        label "Edit"
      } to edit(uname)
    };
    div square {
      link {
        label "Phone Book"
      } to phoneBook(uname)
    };
    div square {
      link {
        label "Logout"
      } to index()
    }
  }

  def action newUser (uname: String, nm: String, pwd: String, ph: String, phnr: String,
                                                                ccard: String): WebPage {
      let x = assume Authenticated(uname) in (insert {
        username = uname,
        name = nm,
        password = pwd,
        photo = ph,
        phone = str2int(phnr),
        creditCardNumber = ccard
      } in User);
      index()
    }

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

  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 "CreditCard: ";
      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 userDetails (logged: {x: String | Authenticated(x)}, uname: String) {
    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;
    br;
    link {
      label "Phone Book"
    } to phoneBook(logged)
  }

  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