annotate src/ur/openidUser.urs @ 32:90b8ce9be9f5

Change some field names and update utest
author Adam Chlipala <adam@chlipala.net>
date Thu, 21 Apr 2011 13:24:55 -0400
parents 1be573ac8e2b
children df258dbf4739
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
adam@18 12 (* Instantiate this functor to create your customized authentication scheme. *)
adam@16 13 functor Make(M: sig
adam@16 14 con cols :: {Type}
adam@16 15 constraint [Id] ~ cols
adam@17 16 val folder : folder cols
adam@17 17 val inj : $(map sql_injectable cols)
adam@18 18 (* Extra columns of profile information to include in the user
adam@18 19 * database table *)
adam@16 20
adam@17 21 type creationState
adam@18 22 (* The type of client-side state used while soliciting sign-up
adam@18 23 * input *)
adam@17 24 type creationData
adam@18 25 (* A functional representation of the latest client-side state *)
adam@18 26
adam@17 27 val creationState : transaction creationState
adam@18 28 (* Create some fresh client-side state. *)
adam@18 29
adam@17 30 val render : creationState -> xtable
adam@18 31 (* Display widgets. *)
adam@18 32
adam@20 33 val ready : creationState -> signal bool
adam@20 34 (* Is the data ready to send? *)
adam@20 35
adam@17 36 val tabulate : creationState -> signal creationData
adam@18 37 (* Functionalize current state. *)
adam@18 38
adam@18 39 val choose : sql_table ([Id = string] ++ cols) [Pkey = [Id]]
adam@28 40 -> creationData -> transaction (choose_result $cols)
adam@18 41 (* Use functionalized state to choose initial column values,
adam@18 42 * given a handle to the users table. *)
adam@17 43
adam@16 44 val sessionLifetime : int
adam@16 45 (* Number of seconds a session may live *)
adam@16 46
adam@16 47 val afterLogout : url
adam@16 48 (* Where to send the user after he logs out *)
adam@16 49
adam@16 50 val secureCookies : bool
adam@18 51 (* Should authentication cookies be restricted to SSL
adam@18 52 * connections? *)
adam@16 53
adam@16 54 val association : Openid.association_mode
adam@16 55 (* OpenID cryptography preferences *)
adam@16 56
adam@16 57 val realm : option string
adam@18 58 (* See end of [Openid] module's documentation for the meaning
adam@18 59 * of realms. *)
adam@17 60
adam@17 61 val formClass : css_class
adam@18 62 (* CSS class for <table>, <th>, and <td> elements used in
adam@18 63 * sign-up form *)
adam@23 64
adam@23 65 val fakeId : option string
adam@23 66 (* If set, this string is always accepted as a verified
adam@23 67 * identifier, which can be useful during development (say,
adam@23 68 * when you're off-network). *)
kkallio@31 69
adam@32 70 val ctlDisplay : {User : {Status : xbody,
adam@32 71 (* Anything extra to display to represent the logged-in user's status *)
adam@32 72 Logout : xbody
adam@32 73 (* Text for link to log out *)},
adam@32 74 Guest : {Status : xbody,
adam@32 75 (* What to show in the place where a logged-in user's status would be *)
adam@32 76 Signup : xbody
adam@32 77 (* Text for link to sign up *)}}
adam@16 78 end) : sig
adam@16 79
adam@16 80 type user
adam@28 81 val eq_user : eq user
adam@16 82 val show_user : show user
adam@28 83 val read_user : read user
adam@16 84 val inj_user : sql_injectable_prim user
adam@18 85 (* The abstract type of user IDs. It's really [string], but this is only
adam@18 86 * exposed via some standard type class instances. *)
adam@16 87
adam@16 88 table user : ([Id = user] ++ M.cols)
adam@16 89 PRIMARY KEY Id
adam@16 90
adam@16 91 val current : transaction (option user)
adam@18 92 (* Figure out which, if any, user is logged in on this connection. *)
adam@16 93
adam@25 94 val main : (string -> xbody -> transaction page) -> transaction {Status : xbody,
adam@25 95 Other : xbody}
adam@18 96 (* Pass in your generic page template; get out the HTML snippet for user
adam@18 97 * management, suitable for, e.g., inclusion in your standard page
adam@25 98 * header. The output gives a "status" chunk, which will either be a login
adam@25 99 * form or a message about which user is logged in; and an "other" chunk,
adam@25 100 * which will be a log out or sign up link. *)
adam@16 101
adam@16 102 end
adam@26 103
adam@26 104 (* Functor outputs will contain buttons specialized to particular well-known
adam@26 105 * OpenID providers. Use these CSS classes to style those buttons. *)
adam@26 106 style aol
adam@26 107 style google
adam@26 108 style myspace
adam@26 109 style yahoo
adam@26 110
adam@26 111 (* This style is used by forms containing the above buttons. *)
adam@26 112 style provider