From 72664fd130cf983bc2d3cbc0aacd6776625a71b1 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 2 Nov 2009 15:48:06 -0500 Subject: Start of Decision --- demo/more/bid.ur | 2 ++ demo/more/bid.urs | 4 ++++ demo/more/conference.ur | 60 +++++++++++++++++++++++++++++++++++++++--------- demo/more/conference.urp | 1 + demo/more/conference.urs | 26 ++++++++++++++++++--- demo/more/conference1.ur | 13 ++++++++--- demo/more/decision.ur | 55 ++++++++++++++++++++++++++++++++++++++++++++ demo/more/decision.urs | 11 +++++++++ demo/more/meta.ur | 9 ++++++++ demo/more/meta.urs | 8 +++++++ src/elaborate.sml | 44 ++++++++++++++++++++++++----------- 11 files changed, 203 insertions(+), 30 deletions(-) create mode 100644 demo/more/decision.ur create mode 100644 demo/more/decision.urs diff --git a/demo/more/bid.ur b/demo/more/bid.ur index 171dbedb..50645f38 100644 --- a/demo/more/bid.ur +++ b/demo/more/bid.ur @@ -1,3 +1,5 @@ +con fields userId paperId = [User = userId, Paper = paperId] + functor Make(M : Conference.INPUT) = struct open M diff --git a/demo/more/bid.urs b/demo/more/bid.urs index f731f9ba..1504c1b7 100644 --- a/demo/more/bid.urs +++ b/demo/more/bid.urs @@ -1,3 +1,7 @@ +con fields :: Type -> Type -> {Type} + functor Make (M : Conference.INPUT) : Conference.OUTPUT where con paper = M.paper where con userId = M.userId where con paperId = M.paperId + where con yourPaperTables = [Assignment + = fields M.userId M.paperId] diff --git a/demo/more/conference.ur b/demo/more/conference.ur index 3c262e15..8f6dff2a 100644 --- a/demo/more/conference.ur +++ b/demo/more/conference.ur @@ -45,19 +45,26 @@ open Meta functor Make(M : sig con paper :: {(Type * Type)} constraint [Id, Document, Authors] ~ paper - val paper : $(map meta 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 review) + val review : $(map Meta.meta review) val reviewFolder : folder review val submissionDeadline : time - val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper) -> xml ([Body] ++ ctx) [] [] + val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate) + -> xml ([Body] ++ ctx) [] [] - functor Make (M : INPUT where con paper = map fst paper) - : OUTPUT where con paper = map fst paper + functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate) + : OUTPUT where con paper = map fst paper ++ paperPrivate where con userId = M.userId where con paperId = M.paperId end) = struct @@ -67,7 +74,7 @@ functor Make(M : sig CONSTRAINT Nam UNIQUE Nam sequence userId - con paper = [Id = int, Document = blob] ++ map fst M.paper + con paper = [Id = int, Document = blob] ++ map fst M.paper ++ M.paperPrivate table paper : paper PRIMARY KEY Id sequence paperId @@ -254,7 +261,8 @@ functor Make(M : sig else id <- nextval paperId; dml (insert paper ({Id = sql_inject id, Document = sql_inject (fileData r.Document)} - ++ ensql M.paper (r -- #Authors -- #Document) M.paperFolder)); + ++ ensql M.paper (r -- #Authors -- #Document) M.paperFolder + ++ initialize M.paperPrivate M.paperPrivateFolder)); List.app (fn uid => case uid of None => error Impossible empty uid! @@ -287,10 +295,12 @@ functor Make(M : sig end - and listPapers [tabs] [[Paper] ~ tabs] (q : sql_query ([Paper = [Id = int] ++ map fst M.paper] ++ tabs) []) = + and listPapers [tabs] [[Paper] ~ tabs] + (q : sql_query ([Paper = [Id = int] ++ map fst M.paper ++ M.paperPrivate] ++ tabs) []) = checkOnPc; ps <- queryX q - (fn r =>
  • {M.summarizePaper (r.Paper -- #Id)}
    • ); + (fn r =>
  • {M.summarizePaper (r.Paper -- #Id)} +
    • ); return

    All Papers

    @@ -301,7 +311,7 @@ functor Make(M : sig and all () = checkOnPc; - listPapers (SELECT paper.Id, paper.{{map fst M.paper}} FROM paper) + listPapers (SELECT paper.Id, paper.{{map fst M.paper ++ M.paperPrivate}} FROM paper) and your () = me <- getLogin; @@ -310,7 +320,10 @@ functor Make(M : sig Where = (WHERE TRUE), GroupBy = sql_subset_all [_], Having = (WHERE TRUE), - SelectFields = sql_subset [[Paper = ([Id = _] ++ map fst M.paper, _)] + SelectFields = sql_subset [[Paper = + ([Id = _] + ++ map fst M.paper + ++ M.paperPrivate, _)] ++ map (fn ts => ([], ts)) O.yourPaperTables], SelectExps = {}}, @@ -412,3 +425,28 @@ functor Make(M : sig | Some r => returnBlob r.Paper.Document (blessMime "application/pdf") 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) + = struct + open M + open O1 + + val linksForPc = {O1.linksForPc}{O2.linksForPc} + val linksForChair = {O1.linksForChair}{O2.linksForChair} + + con yourPaperTables = O1.yourPaperTables ++ O2.yourPaperTables + constraint [Paper] ~ yourPaperTables + + fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper] + uid (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) = + O2.joinYourPaper uid (O1.joinYourPaper uid fi) + end diff --git a/demo/more/conference.urp b/demo/more/conference.urp index 9e0d8eaa..663fd681 100644 --- a/demo/more/conference.urp +++ b/demo/more/conference.urp @@ -12,3 +12,4 @@ select checkGroup expandable bid +decision diff --git a/demo/more/conference.urs b/demo/more/conference.urs index 16e6732f..8ecb1692 100644 --- a/demo/more/conference.urs +++ b/demo/more/conference.urs @@ -46,16 +46,23 @@ functor Make(M : sig 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) -> xml ([Body] ++ ctx) [] [] + val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate) + -> xml ([Body] ++ ctx) [] [] - functor Make (M : INPUT where con paper = map fst paper) - : OUTPUT where con paper = map fst paper + functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate) + : OUTPUT where con paper = map fst paper ++ paperPrivate where con userId = M.userId where con paperId = M.paperId end) : sig @@ -63,3 +70,16 @@ functor Make(M : 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 diff --git a/demo/more/conference1.ur b/demo/more/conference1.ur index 501788a8..55aa1241 100644 --- a/demo/more/conference1.ur +++ b/demo/more/conference1.ur @@ -3,14 +3,21 @@ open ConferenceFields open Conference.Make(struct val paper = {Title = title, Abstract = abstract} + val paperPrivate = {Decision = Decision.decision} val review = {Rating = dropdown "Rating" (#"A" :: #"B" :: #"C" :: #"D" :: []), CommentsForAuthors = commentsForAuthors} val submissionDeadline = readError "2009-11-22 23:59:59" - fun summarizePaper [ctx] [[Body] ~ ctx] r = cdata r.Title + fun summarizePaper [ctx] [[Body] ~ ctx] r = txt r.Title - functor Make (M : Conference.INPUT where con paper = [Title = string, Abstract = string]) = struct - open Bid.Make(M) + functor Make (M : Conference.INPUT where con paper = _) = struct + open Conference.Join(struct + structure O1 = Bid.Make(M) + structure O2 = Decision.Make(struct + con paperOther = _ + open M + end) + end) end end) diff --git a/demo/more/decision.ur b/demo/more/decision.ur new file mode 100644 index 00000000..986658e8 --- /dev/null +++ b/demo/more/decision.ur @@ -0,0 +1,55 @@ +val decision = {Nam = "Decision", + Initialize = None, + Show = fn bo => cdata (case bo of + None => "?" + | Some True => "Accept" + | Some False => "Reject"), + Inject = _} + +functor Make(M : sig + con paperOther :: {Type} + constraint [Id, Decision] ~ paperOther + include Conference.INPUT + where con paper = [Decision = option bool] ++ paperOther + end) = struct + open M + + val linksForChair = + let + fun makeDecisions () = + ps <- queryX (SELECT paper.Id, paper.Decision, paper.{{M.paperOther}} + FROM paper + ORDER BY paper.Id) + (fn r => + {useMore (summarizePaper (r.Paper -- #Id))} + + + + + + + + ); + return +

    Make acceptance decisions

    + +
    + + + {ps} +
    Paper Decision
    + +
    + in + +
  • Make acceptance decisions
    • +     + end + + val linksForPc = + + con yourPaperTables = [] + constraint [Paper] ~ yourPaperTables + fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper] + uid (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) = fi +end diff --git a/demo/more/decision.urs b/demo/more/decision.urs new file mode 100644 index 00000000..d3ac0d46 --- /dev/null +++ b/demo/more/decision.urs @@ -0,0 +1,11 @@ +val decision : Meta.private (option bool) + +functor Make (M : sig + con paperOther :: {Type} + constraint [Id, Decision] ~ paperOther + include Conference.INPUT + where con paper = [Decision = option bool] ++ paperOther + end) : Conference.OUTPUT where con paper = [Decision = option bool] ++ M.paperOther + where con userId = M.userId + where con paperId = M.paperId + where con yourPaperTables = [] diff --git a/demo/more/meta.ur b/demo/more/meta.ur index 74b5004f..b8a3d584 100644 --- a/demo/more/meta.ur +++ b/demo/more/meta.ur @@ -80,3 +80,12 @@ fun ensql [avail] [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map snd map2 [meta] [snd] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] (fn [ts] meta v => @sql_inject meta.Inject (meta.Parse v)) [_] fl r vs + +con private = fn t :: Type => + {Nam : string, + Initialize : t, + Show : t -> xbody, + Inject : sql_injectable t} + +fun initialize [ts] (r : $(map private ts)) (fl : folder ts) = + mp [private] [sql_exp [] [] []] (fn [t] r => @sql_inject r.Inject r.Initialize) [_] fl r diff --git a/demo/more/meta.urs b/demo/more/meta.urs index 0d3422af..cd3e183a 100644 --- a/demo/more/meta.urs +++ b/demo/more/meta.urs @@ -26,3 +26,11 @@ val allPopulatedTr : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) - val ensql : avail ::: {{Type}} -> ts ::: {(Type * Type)} -> $(map meta ts) -> $(map snd ts) -> folder ts -> $(map (sql_exp avail [] []) (map fst ts)) + +con private = fn t :: Type => + {Nam : string, + Initialize : t, + Show : t -> xbody, + Inject : sql_injectable t} + +val initialize : ts ::: {Type} -> $(map private ts) -> folder ts -> $(map (sql_exp [] [] []) ts) diff --git a/src/elaborate.sml b/src/elaborate.sml index f13f6f1d..ec742ce7 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1996,14 +1996,30 @@ fun dopenConstraints (loc, env, denv) {str, strs} = (strerror, sgnerror)) | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) ((L'.StrVar n, loc), sgn) strs - - val cso = E.projectConstraints env {sgn = sgn, str = st} + + fun collect first (st, sgn) = + case E.projectConstraints env {sgn = sgn, str = st} of + NONE => (if first then + strError env (UnboundStr (loc, str)) + else + (); + []) + | SOME cs => + case #1 (hnormSgn env sgn) of + L'.SgnConst sgis => + foldl (fn (sgi, cs) => + case #1 sgi of + L'.SgiStr (x, _, _) => + (case E.projectStr env {sgn = sgn, str = st, field = x} of + NONE => raise Fail "Elaborate: projectStr in collect" + | SOME sgn' => + List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'), + cs)) + | _ => cs) cs sgis + | _ => cs in - case cso of - NONE => (strError env (UnboundStr (loc, str)); - denv) - | SOME cs => foldl (fn ((c1, c2), denv) => - D.assert env denv (c1, c2)) denv cs + foldl (fn ((c1, c2), denv) => + D.assert env denv (c1, c2)) denv (collect true (st, sgn)) end fun elabSgn_item ((sgi, loc), (env, denv, gs)) = @@ -3445,12 +3461,14 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = ([], (env, denv, gs))) | SOME (n, sgn) => let - val (_, sgn) = foldl (fn (m, (str, sgn)) => - case E.projectStr env {str = str, sgn = sgn, field = m} of - NONE => (strError env (UnboundStr (loc, m)); - (strerror, sgnerror)) - | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) - ((L'.StrVar n, loc), sgn) ms + val (str, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {str = str, sgn = sgn, field = m} of + NONE => (strError env (UnboundStr (loc, m)); + (strerror, sgnerror)) + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) ms + + val sgn = selfifyAt env {str = str, sgn = sgn} val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms} -- cgit v1.2.3