Mercurial > urweb

annotate demo/more/conference.urs @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
rev   line source
adamc@1022 1 signature INPUT = sig
adamc@1023 2 con paper :: {Type}
adamc@1022 3 constraint [Id, Document] ~ paper
adamc@1022 4
adamc@1022 5 type userId
adamc@1022 6 val userId_inj : sql_injectable_prim userId
adamc@1022 7 table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool}
adamc@1022 8 PRIMARY KEY Id,
adamc@1022 9 CONSTRAINT Nam UNIQUE Nam
adamc@1022 10
adamc@1022 11 type paperId
adamc@1022 12 val paperId_inj : sql_injectable_prim paperId
adamc@1023 13 val paperId_show : show paperId
adamc@1023 14 val paperId_read : read paperId
adamc@1025 15 val paperId_eq : eq paperId
adamc@1023 16 table paper : ([Id = paperId, Document = blob] ++ paper)
adamc@1022 17 PRIMARY KEY Id
adamc@1022 18
adamc@1032 19 con review :: {Type}
adamc@1032 20 constraint [Paper, User] ~ review
adamc@1032 21 table review : ([Paper = paperId, User = userId] ++ review)
adamc@1032 22 PRIMARY KEY (Paper, User)
adamc@1032 23
adamc@1022 24 val checkLogin : transaction (option {Id : userId, Nam : string, Chair : bool, OnPc : bool})
adamc@1022 25 val getLogin : transaction {Id : userId, Nam : string, Chair : bool, OnPc : bool}
adamc@1023 26 val getPcLogin : transaction {Id : userId, Nam : string, Chair : bool}
adamc@1025 27 val checkChair : transaction unit
adamc@1023 28 val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $paper -> xml ([Body] ++ ctx) [] []
adamc@1022 29 end
adamc@1022 30
adamc@1022 31 signature OUTPUT = sig
adamc@1023 32 con paper :: {Type}
adamc@1022 33 type userId
adamc@1022 34 type paperId
adamc@1022 35
adamc@1022 36 val linksForPc : xbody
adamc@1025 37 val linksForChair : xbody
adamc@1022 38
adamc@1022 39 con yourPaperTables :: {{Type}}
adamc@1022 40 constraint [Paper] ~ yourPaperTables
adamc@1022 41 val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type}
adamc@1022 42 -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] =>
adamc@1027 43 userId (* Current user *)
adamc@1027 44 -> sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)
adamc@1022 45 -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs)
adamc@1022 46 end
adamc@1022 47
adamc@1001 48 functor Make(M : sig
adamc@1003 49 con paper :: {(Type * Type)}
adamc@1010 50 constraint [Id, Document, Authors] ~ paper
adamc@1004 51 val paper : $(map Meta.meta paper)
adamc@1007 52 val paperFolder : folder paper
adamc@1003 53
adamc@1030 54 con paperPrivate :: {Type}
adamc@1030 55 constraint [Id, Document, Authors] ~ paperPrivate
adamc@1030 56 constraint paper ~ paperPrivate
adamc@1030 57 val paperPrivate : $(map Meta.private paperPrivate)
adamc@1030 58 val paperPrivateFolder : folder paperPrivate
adamc@1030 59
adamc@1001 60 con review :: {(Type * Type)}
adamc@1003 61 constraint [Paper, User] ~ review
adamc@1004 62 val review : $(map Meta.meta review)
adamc@1011 63 val reviewFolder : folder review
adamc@1006 64
adamc@1006 65 val submissionDeadline : time
adamc@1030 66 val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate)
adamc@1030 67 -> xml ([Body] ++ ctx) [] []
adamc@1022 68
adamc@1032 69 functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate
adamc@1032 70 where con review = map fst review)
adamc@1030 71 : OUTPUT where con paper = map fst paper ++ paperPrivate
adamc@1023 72 where con userId = M.userId
adamc@1022 73 where con paperId = M.paperId
adamc@1001 74 end) : sig
adamc@1001 75
adamc@1001 76 val main : unit -> transaction page
adamc@1001 77
adamc@1001 78 end
adamc@1030 79
adamc@1030 80 functor Join(M : sig
adamc@1030 81 structure O1 : OUTPUT
adamc@1030 82
adamc@1030 83 structure O2 : OUTPUT where con paper = O1.paper
adamc@1030 84 where con userId = O1.userId
adamc@1030 85 where con paperId = O1.paperId
adamc@1030 86
adamc@1030 87 constraint O1.yourPaperTables ~ O2.yourPaperTables
adamc@1030 88 end) : OUTPUT where con paper = M.O1.paper
adamc@1030 89 where con userId = M.O1.userId
adamc@1030 90 where con paperId = M.O1.paperId
adamc@1030 91 where con yourPaperTables = M.O1.yourPaperTables ++ M.O2.yourPaperTables