Mercurial > urweb

annotate demo/more/conference.urs @ 1324:d596c7002ad8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More accurate/conservative leaky type detection in CjrPrint
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Nov 2010 15:06:11 -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