From e20e964083a048ad4cbb88cc1af3790694f51dfa Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 1 Nov 2009 10:20:20 -0500 Subject: Bidding interface --- demo/more/conference.urs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'demo/more/conference.urs') diff --git a/demo/more/conference.urs b/demo/more/conference.urs index 226e9768..f9729851 100644 --- a/demo/more/conference.urs +++ b/demo/more/conference.urs @@ -1,5 +1,5 @@ signature INPUT = sig - con paper :: {(Type * Type)} + con paper :: {Type} constraint [Id, Document] ~ paper type userId @@ -10,14 +10,19 @@ signature INPUT = sig type paperId val paperId_inj : sql_injectable_prim paperId - table paper : ([Id = paperId, Document = blob] ++ map fst paper) + val paperId_show : show paperId + val paperId_read : read paperId + table paper : ([Id = paperId, Document = blob] ++ paper) PRIMARY KEY Id 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 summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $paper -> xml ([Body] ++ ctx) [] [] end signature OUTPUT = sig + con paper :: {Type} type userId type paperId @@ -43,10 +48,11 @@ functor Make(M : sig val reviewFolder : folder review val submissionDeadline : time - val summarizePaper : $(map fst paper) -> xbody + val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper) -> xml ([Body] ++ ctx) [] [] - functor Make (M : INPUT where con paper = paper) - : OUTPUT where con userId = M.userId + functor Make (M : INPUT where con paper = map fst paper) + : OUTPUT where con paper = map fst paper + where con userId = M.userId where con paperId = M.paperId end) : sig -- cgit v1.2.3