annotate src/ur/openidUser.urs @ 64:81632203928f

Fix 'hidden' constraint
author Adam Chlipala <adam@chlipala.net>
date Wed, 11 Dec 2013 17:11:32 -0500
parents a984dc1c8954
children
rev   line source
adam@18 1 (* This module provides generic user authentication functionality, backed by
adam@18 2 * OpenID authentication. Each account (named with a short alphanumeric string)
adam@18 3 * is associated with one or more OpenID identifiers, any of which may be used
adam@18 4 * to log in as that user. This module provides all the code you need to sign
adam@18 5 * users up, log them in, and check which user is logged in.
adam@18 6 *
adam@18 7 * Module author: Adam Chlipala
adam@18 8 *)
adam@18 9
adam@28 10 datatype choose_result a = Success of a | Failure of string
adam@28 11
kkallio@35 12 (* Formatting options for the gui elements and controls. *)
kkallio@35 13 signature CTLDISPLAY = sig
kkallio@35 14
kkallio@35 15 val formatUser : xbody -> xbody
kkallio@35 16 (* Format the display of the logged on user *)
kkallio@35 17
greenrd@48 18 val formatLogout : ($([]) -> transaction page) -> xbody
greenrd@48 19 (* Format the logout button *)
kkallio@35 20
kkallio@35 21 val formatSignup : url -> xbody
kkallio@35 22 (* Format the signup link *)
kkallio@35 23
kkallio@35 24 val formatLogon : ({User : string} -> transaction page) -> xbody
adam@37 25 (* Format the login form *)
kkallio@35 26 end
kkallio@35 27
kkallio@35 28 (* Some reasonable default gui control formats for programmers in a hurry. *)
kkallio@35 29 structure DefaultDisplay : CTLDISPLAY
kkallio@35 30
kkallio@35 31
adam@18 32 (* Instantiate this functor to create your customized authentication scheme. *)
adam@16 33 functor Make(M: sig
adam@16 34 con cols :: {Type}
adam@16 35 constraint [Id] ~ cols
adam@17 36 val folder : folder cols
adam@17 37 val inj : $(map sql_injectable cols)
adam@18 38 (* Extra columns of profile information to include in the user
adam@18 39 * database table *)
adam@16 40
adam@17 41 type creationState
adam@18 42 (* The type of client-side state used while soliciting sign-up
adam@18 43 * input *)
adam@17 44 type creationData
adam@18 45 (* A functional representation of the latest client-side state *)
adam@18 46
adam@17 47 val creationState : transaction creationState
adam@18 48 (* Create some fresh client-side state. *)
adam@18 49
adam@17 50 val render : creationState -> xtable
adam@18 51 (* Display widgets. *)
adam@18 52
adam@20 53 val ready : creationState -> signal bool
adam@20 54 (* Is the data ready to send? *)
adam@20 55
adam@17 56 val tabulate : creationState -> signal creationData
adam@18 57 (* Functionalize current state. *)
adam@18 58
adam@18 59 val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]]
adam@28 60 -> creationData -> transaction (choose_result $cols)
adam@18 61 (* Use functionalized state to choose initial column values,
adam@18 62 * given a handle to the users table. *)
adam@17 63
adam@16 64 val sessionLifetime : int
adam@16 65 (* Number of seconds a session may live *)
adam@16 66
adam@16 67 val afterLogout : url
adam@16 68 (* Where to send the user after he logs out *)
adam@16 69
adam@16 70 val secureCookies : bool
adam@18 71 (* Should authentication cookies be restricted to SSL
adam@18 72 * connections? *)
adam@16 73
adam@16 74 val association : Openid.association_mode
adam@16 75 (* OpenID cryptography preferences *)
adam@16 76
adam@16 77 val realm : option string
adam@18 78 (* See end of [Openid] module's documentation for the meaning
adam@18 79 * of realms. *)
adam@17 80
adam@17 81 val formClass : css_class
adam@18 82 (* CSS class for <table>, <th>, and <td> elements used in
adam@18 83 * sign-up form *)
adam@23 84
adam@23 85 val fakeId : option string
adam@23 86 (* If set, this string is always accepted as a verified
adam@23 87 * identifier, which can be useful during development (say,
adam@23 88 * when you're off-network). *)
kkallio@35 89
kkallio@35 90 structure CtlDisplay : CTLDISPLAY
kkallio@35 91 (* Tells how to format the GUI elements. *)
adam@16 92 end) : sig
adam@16 93
adam@16 94 type user
adam@28 95 val eq_user : eq user
adam@16 96 val show_user : show user
adam@28 97 val read_user : read user
adam@16 98 val inj_user : sql_injectable_prim user
adam@18 99 (* The abstract type of user IDs. It's really [string], but this is only
adam@18 100 * exposed via some standard type class instances. *)
adam@16 101
adam@16 102 table user : ([Id = user] ++ M.cols)
adam@16 103 PRIMARY KEY Id
adam@16 104
adam@16 105 val current : transaction (option user)
adam@18 106 (* Figure out which, if any, user is logged in on this connection. *)
adam@16 107
adam@50 108 val renew : transaction (option user)
adam@50 109 (* Like [current], but also resets the expiration time of the user's
adam@50 110 * session, if one is found. *)
adam@50 111
kkallio@35 112
adam@25 113 val main : (string -> xbody -> transaction page) -> transaction {Status : xbody,
greenrd@48 114 Other : {Url : option url, Xml : xbody}}
kkallio@35 115
adam@18 116 (* Pass in your generic page template; get out the HTML snippet for user
adam@18 117 * management, suitable for, e.g., inclusion in your standard page
adam@25 118 * header. The output gives a "status" chunk, which will either be a login
adam@25 119 * form or a message about which user is logged in; and an "other" chunk,
greenrd@48 120 * which will be a log out button or sign up link. In the case of "other",
greenrd@48 121 * the link itself (if available) is also provided for cases when one
greenrd@48 122 * format is not enough. *)
kkallio@35 123
adam@16 124 end
adam@26 125
adam@26 126 (* Functor outputs will contain buttons specialized to particular well-known
adam@26 127 * OpenID providers. Use these CSS classes to style those buttons. *)
adam@26 128 style aol
adam@26 129 style google
adam@26 130 style myspace
adam@26 131 style yahoo
adam@26 132
adam@26 133 (* This style is used by forms containing the above buttons. *)
adam@26 134 style provider