adam@18: (* This module provides generic user authentication functionality, backed by
adam@18:  * OpenID authentication.  Each account (named with a short alphanumeric string)
adam@18:  * is associated with one or more OpenID identifiers, any of which may be used
adam@18:  * to log in as that user.  This module provides all the code you need to sign
adam@18:  * users up, log them in, and check which user is logged in.
adam@18:  *
adam@18:  * Module author: Adam Chlipala
adam@18:  *)
adam@18: 
adam@28: datatype choose_result a = Success of a | Failure of string
adam@28: 
kkallio@35: (* Formatting options for the gui elements and controls. *)
kkallio@35: signature CTLDISPLAY = sig
kkallio@35: 
kkallio@35:     val formatUser : xbody -> xbody
kkallio@35:     (* Format the display of the logged on user *)
kkallio@35:                               
kkallio@35:     val formatLogout : url -> xbody
kkallio@35:     (* Format the logout link *)
kkallio@35: 
kkallio@35:     val formatSignup : url -> xbody
kkallio@35:     (* Format the signup link *)
kkallio@35: 
kkallio@35:     val formatLogon : ({User : string} -> transaction page) -> xbody
adam@37:     (* Format the login form *)
kkallio@35: end
kkallio@35: 
kkallio@35: (* Some reasonable default gui control formats for programmers in a hurry. *)
kkallio@35: structure DefaultDisplay : CTLDISPLAY
kkallio@35: 
kkallio@35: 
adam@18: (* Instantiate this functor to create your customized authentication scheme. *)
adam@16: functor Make(M: sig
adam@16:                  con cols :: {Type}
adam@16:                  constraint [Id] ~ cols
adam@17:                  val folder : folder cols
adam@17:                  val inj : $(map sql_injectable cols)
adam@18:                  (* Extra columns of profile information to include in the user
adam@18:                   * database table *)
adam@16: 
adam@17:                  type creationState
adam@18:                  (* The type of client-side state used while soliciting sign-up
adam@18:                   * input *)
adam@17:                  type creationData
adam@18:                  (* A functional representation of the latest client-side state *)
adam@18: 
adam@17:                  val creationState : transaction creationState
adam@18:                  (* Create some fresh client-side state. *)
adam@18: 
adam@17:                  val render : creationState -> xtable
adam@18:                  (* Display widgets. *)
adam@18: 
adam@20:                  val ready : creationState -> signal bool
adam@20:                  (* Is the data ready to send? *)
adam@20: 
adam@17:                  val tabulate : creationState -> signal creationData
adam@18:                  (* Functionalize current state. *)
adam@18: 
adam@18:                  val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]]
adam@28:                               -> creationData -> transaction (choose_result $cols)
adam@18:                  (* Use functionalized state to choose initial column values,
adam@18:                   * given a handle to the users table. *)
adam@17: 
adam@16:                  val sessionLifetime : int
adam@16:                  (* Number of seconds a session may live *)
adam@16: 
adam@16:                  val afterLogout : url
adam@16:                  (* Where to send the user after he logs out *)
adam@16: 
adam@16:                  val secureCookies : bool
adam@18:                  (* Should authentication cookies be restricted to SSL
adam@18:                   * connections? *)
adam@16: 
adam@16:                  val association : Openid.association_mode
adam@16:                  (* OpenID cryptography preferences *)
adam@16: 
adam@16:                  val realm : option string
adam@18:                  (* See end of [Openid] module's documentation for the meaning
adam@18:                   * of realms. *)
adam@17: 
adam@17:                  val formClass : css_class
adam@18:                  (* CSS class for <table>, <th>, and <td> elements used in
adam@18:                   * sign-up form *)
adam@23: 
adam@23:                  val fakeId : option string
adam@23:                  (* If set, this string is always accepted as a verified
adam@23:                   * identifier, which can be useful during development (say,
adam@23:                   * when you're off-network). *)
kkallio@35: 
kkallio@35:                  structure CtlDisplay : CTLDISPLAY
kkallio@35:                  (* Tells how to format the GUI elements. *)
adam@16:              end) : sig
adam@16: 
adam@16:     type user
adam@28:     val eq_user : eq user
adam@16:     val show_user : show user
adam@28:     val read_user : read user
adam@16:     val inj_user : sql_injectable_prim user
adam@18:     (* The abstract type of user IDs.  It's really [string], but this is only
adam@18:      * exposed via some standard type class instances. *)
adam@16: 
adam@16:     table user : ([Id = user] ++ M.cols)
adam@16:       PRIMARY KEY Id
adam@16: 
adam@16:     val current : transaction (option user)
adam@18:     (* Figure out which, if any, user is logged in on this connection. *)
adam@16: 
kkallio@35: 
adam@25:     val main : (string -> xbody -> transaction page) -> transaction {Status : xbody,
kkallio@35:                                                                      Other : {Url : url, Xml : xbody}}
kkallio@35: 
adam@18:     (* Pass in your generic page template; get out the HTML snippet for user
adam@18:      * management, suitable for, e.g., inclusion in your standard page
adam@25:      * header.  The output gives a "status" chunk, which will either be a login
adam@25:      * form or a message about which user is logged in; and an "other" chunk,
kkallio@36:      * which will be a log out or sign up link. In the case "other", the link
kkallio@36:      * itself is also provided for cases when one format is not enough. *)
kkallio@35:                              
adam@16: end
adam@26: 
adam@26: (* Functor outputs will contain buttons specialized to particular well-known
adam@26:  * OpenID providers.  Use these CSS classes to style those buttons. *)
adam@26: style aol
adam@26: style google
adam@26: style myspace
adam@26: style yahoo
adam@26: 
adam@26: (* This style is used by forms containing the above buttons. *)
adam@26: style provider