Mercurial > urweb
view demo/more/conference.urs @ 1034:a779402841f6
Hooks for measuring how much interesting proving is going on in elaboration
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 17 Nov 2009 12:44:14 -0500 |
parents | 5d9f47124c4c |
children |
line wrap: on
line source
signature INPUT = sig con paper :: {Type} constraint [Id, Document] ~ paper type userId val userId_inj : sql_injectable_prim userId table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool} PRIMARY KEY Id, CONSTRAINT Nam UNIQUE Nam type paperId val paperId_inj : sql_injectable_prim paperId val paperId_show : show paperId val paperId_read : read paperId val paperId_eq : eq paperId table paper : ([Id = paperId, Document = blob] ++ paper) PRIMARY KEY Id con review :: {Type} constraint [Paper, User] ~ review table review : ([Paper = paperId, User = userId] ++ review) PRIMARY KEY (Paper, User) val checkLogin : transaction (option {Id : userId, Nam : string, Chair : bool, OnPc : bool}) val getLogin : transaction {Id : userId, Nam : string, Chair : bool, OnPc : bool} val getPcLogin : transaction {Id : userId, Nam : string, Chair : bool} val checkChair : transaction unit val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $paper -> xml ([Body] ++ ctx) [] [] end signature OUTPUT = sig con paper :: {Type} type userId type paperId val linksForPc : xbody val linksForChair : xbody con yourPaperTables :: {{Type}} constraint [Paper] ~ yourPaperTables val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type} -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] => userId (* Current user *) -> sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs) -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs) end functor Make(M : sig con paper :: {(Type * Type)} constraint [Id, Document, Authors] ~ paper val paper : $(map Meta.meta paper) val paperFolder : folder paper con paperPrivate :: {Type} constraint [Id, Document, Authors] ~ paperPrivate constraint paper ~ paperPrivate val paperPrivate : $(map Meta.private paperPrivate) val paperPrivateFolder : folder paperPrivate con review :: {(Type * Type)} constraint [Paper, User] ~ review val review : $(map Meta.meta review) val reviewFolder : folder review val submissionDeadline : time val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate) -> xml ([Body] ++ ctx) [] [] functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate where con review = map fst review) : OUTPUT where con paper = map fst paper ++ paperPrivate where con userId = M.userId where con paperId = M.paperId end) : sig val main : unit -> transaction page end functor Join(M : sig structure O1 : OUTPUT structure O2 : OUTPUT where con paper = O1.paper where con userId = O1.userId where con paperId = O1.paperId constraint O1.yourPaperTables ~ O2.yourPaperTables end) : OUTPUT where con paper = M.O1.paper where con userId = M.O1.userId where con paperId = M.O1.paperId where con yourPaperTables = M.O1.yourPaperTables ++ M.O2.yourPaperTables