open User

table rootAdmin : { User : user }
  PRIMARY KEY User,
  CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)

task initialize = fn () =>
    b <- nonempty rootAdmin;
    if b then
        return ()
    else
        dml (INSERT INTO rootAdmin (User) VALUES ({[root]}))

type course = int
sequence courseIds
table course : { Id : course, Nam : string }
  PRIMARY KEY Id

policy sendClient (SELECT * FROM course)

table instructor : { Course : course, User : user}
  PRIMARY KEY (Course, User),
  CONSTRAINT Course FOREIGN KEY Course REFERENCES course(Id),
  CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)

policy sendClient (SELECT * FROM instructor)

table ta : { Course : course, User : user}
  PRIMARY KEY (Course, User),
  CONSTRAINT Course FOREIGN KEY Course REFERENCES course(Id),
  CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)

policy sendClient (SELECT * FROM ta)

table student : { Course : course, User : user, Grade : option string }
  PRIMARY KEY (Course, User),
  CONSTRAINT Course FOREIGN KEY Course REFERENCES course(Id),
  CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)

fun adminMay [fs] [ks] (t : sql_table fs ks) =
    also (sendClient (SELECT *
                      FROM t, rootAdmin, user
                      WHERE rootAdmin.User = user.Id
                        AND known(user.Pass)))
    (also (mayInsert (SELECT *
                      FROM t AS New, rootAdmin, user
                      WHERE rootAdmin.User = user.Id
                        AND known(user.Pass)))
          (also (mayDelete (SELECT *
                            FROM t AS Old, rootAdmin, user
                            WHERE rootAdmin.User = user.Id
                              AND known(user.Pass)))
                (mayUpdate (SELECT *
                            FROM t AS New, t AS Old, rootAdmin, user
                            WHERE rootAdmin.User = user.Id
                              AND known(user.Pass)))))

policy adminMay course
policy adminMay instructor
policy adminMay ta
policy adminMay student

fun instructorMay [fs] [[Course] ~ fs] [ks] (t : sql_table ([Course = course] ++ fs) ks) =
    also (sendClient (SELECT *
                      FROM t, instructor, user
                      WHERE instructor.Course = t.Course
                        AND instructor.User = user.Id
                        AND known(user.Pass)))
    (also (mayInsert (SELECT *
                      FROM t AS New, instructor, user
                      WHERE instructor.Course = New.Course
                        AND instructor.User = user.Id
                        AND known(user.Pass)))
     (also (mayDelete (SELECT *
                       FROM t AS Old, instructor, user
                       WHERE instructor.Course = Old.Course
                         AND instructor.User = user.Id
                         AND known(user.Pass)))
           (mayUpdate (SELECT *
                       FROM t AS Old, t AS New, instructor, user
                       WHERE instructor.Course = Old.Course
                         AND instructor.User = user.Id
                         AND New.Course = Old.Course
                         AND known(user.Pass)))))

policy instructorMay ta
policy instructorMay student

policy sendClient (SELECT *
                   FROM student, ta, user
                   WHERE student.Course = ta.Course
                     AND user.Id = ta.User
                     AND known(user.Pass))

policy sendClient (SELECT *
                   FROM student, user
                   WHERE user.Id = student.User
                     AND known(user.Pass))

policy mayDelete (SELECT *
                  FROM student AS Old, user
                  WHERE user.Id = Old.User
                    AND known(user.Pass))
       
fun isAdmin u =
    oneRowE1 (SELECT COUNT( * ) > 0
              FROM rootAdmin
              WHERE rootAdmin.User = {[u]})

fun amAdmin () =
    u <- User.userId ();
    case u of
        None => return False
      | Some u => isAdmin u

fun wrap titl bod =
    bl <- User.blurb ();
    return <xml>
      <head>
        <title>Gradebook - {[titl]}</title>
      </head>

      <body>
        {bl}

        <h1>{[titl]}</h1>

        {bod}
      </body>
    </xml>

fun instructorFor u cid =
    oneRowE1 (SELECT COUNT( * ) > 0
              FROM instructor
              WHERE instructor.Course = {[cid]}
                AND instructor.User = {[u]})

fun taFor u cid =
    oneRowE1 (SELECT COUNT( * ) > 0
              FROM ta
              WHERE ta.Course = {[cid]}
                AND ta.User = {[u]})

datatype level = Nothing | Read | Write | Admin

fun mayAdmin lv =
    case lv of
        Admin => True
      | _ => False

fun mayWrite lv =
    case lv of
        Admin => True
      | Write => True
      | _ => False

fun mayRead lv =
    case lv of
        Admin => True
      | Write => True
      | Read => True
      | _ => False

fun level cid =
    u <- User.userId ();
    case u of
        None => return Nothing
      | Some u =>
        b <- isAdmin u;
        if b then
            return Admin
        else
            b <- instructorFor u cid;
            if b then
                return Write
            else
                b <- taFor u cid;
                return (if b then
                            Read
                        else
                            Nothing)

fun courseInfo cid =
    let
        fun ok lv =
            name <- oneRowE1 (SELECT (course.Nam)
                              FROM course
                              WHERE course.Id = {[cid]});
            sts <- queryX (SELECT user.Id, user.Nam, student.Grade
                           FROM student, user
                           WHERE student.Course = {[cid]}
                             AND student.User = user.Id
                           ORDER BY user.Nam)
                          (fn r =>
                              let
                                  fun setGrade r' =
                                      lv <- level cid;
                                      if mayWrite lv then
                                          dml (UPDATE student
                                               SET Grade = {[Some r'.Grade]}
                                               WHERE Course = {[cid]}
                                                 AND User = {[r.User.Id]});
                                          ok lv
                                      else
                                          error <xml>You are not authorized to set grades for that course.</xml>
                              in
                                  <xml><tr>
                                    <td>{[r.User.Nam]}</td>
                                    <td>{[r.Student.Grade]}</td>
                                    {if mayWrite lv then
                                         <xml><td><form><textbox{#Grade}/>
                                           <submit value="Change" action={setGrade}/></form></td></xml>
                                     else
                                         <xml/>}
                                  </tr></xml>
                              end);

            ins <- queryX1 (SELECT user.Id, user.Nam
                            FROM instructor, user
                            WHERE instructor.Course = {[cid]}
                              AND instructor.User = user.Id
                            ORDER BY user.Nam)
                           (fn r =>
                               let
                                   fun removeInstructor () =
                                       lv <- level cid;
                                       if mayAdmin lv then
                                           dml (DELETE FROM instructor
                                                WHERE Course = {[cid]}
                                                  AND User = {[r.Id]});
                                           ok lv
                                       else
                                           error <xml>You are not allowed to remove instructors.</xml>
                               in
                                   <xml><li>{[r.Nam]}
                                     {if mayAdmin lv then
                                          <xml><form><submit value="Remove" action={removeInstructor}/></form></xml>
                                      else
                                          <xml/>}
                                   </li></xml>
                               end);

            tas <- queryX1 (SELECT user.Id, user.Nam
                            FROM ta, user
                            WHERE ta.Course = {[cid]}
                              AND ta.User = user.Id
                            ORDER BY user.Nam)
                           (fn r =>
                               let
                                   fun removeTa () =
                                       lv <- level cid;
                                       if mayWrite lv then
                                           dml (DELETE FROM ta
                                                WHERE Course = {[cid]}
                                                  AND User = {[r.Id]});
                                           ok lv
                                       else
                                           error <xml>You are not allowed to remove TAs from this course.</xml>
                               in
                                   <xml><li>{[r.Nam]}
                                     {if mayWrite lv then
                                          <xml><form><submit value="Remove" action={removeTa}/></form></xml>
                                      else
                                          <xml/>}
                                   </li></xml>
                               end);
            
            wrap name <xml>
              <h3>Students</h3>

              <table>
                <tr> <th>Name</th> <th>Grade</th> </tr>
                {sts}
              </table>

              <h3>Instructors</h3>

              {ins}

              <h3>TAs</h3>

              {tas}

              {if mayAdmin lv then
                   <xml>
                     <h3>Add an instructor</h3>

                     <form>
                       Name: <textbox{#Nam}/> <submit value="Add" action={addInstructor}/>
                     </form>
                   </xml>
               else
                   <xml/>}

              {if mayWrite lv then
                   <xml>
                     <h3>Register a student</h3>

                     <form>
                       Name: <textbox{#Nam}/> <submit value="Add" action={addStudent}/>
                     </form>

                     <h3>Add a TA</h3>

                     <form>
                       Name: <textbox{#Nam}/> <submit value="Add" action={addTa}/>
                     </form>
                   </xml>
               else
                   <xml/>}
            </xml>

        and addStudent r =
            lv <- level cid;
            if mayWrite lv then
                uo <- oneOrNoRowsE1 (SELECT (user.Id)
                                     FROM user
                                     WHERE user.Nam = {[r.Nam]});
                case uo of
                    None => error <xml>User not found</xml>
                  | Some u =>
                    dml (INSERT INTO student (Course, User, Grade)
                         VALUES ({[cid]}, {[u]}, NULL));
                    ok lv
            else
                error <xml>You are not authorized to register students for that course.</xml>

        and addTa r =
            lv <- level cid;
            if mayWrite lv then
                uo <- oneOrNoRowsE1 (SELECT (user.Id)
                                     FROM user
                                     WHERE user.Nam = {[r.Nam]});
                (case uo of
                     None => error <xml>User not found</xml>
                   | Some u =>
                     dml (INSERT INTO ta (Course, User)
                          VALUES ({[cid]}, {[u]}));
                     ok lv)
            else
                error <xml>You are not authorized to add TAs for that course.</xml>

        and addInstructor r =
            lv <- level cid;
            if mayAdmin lv then
                uo <- oneOrNoRowsE1 (SELECT (user.Id)
                                     FROM user
                                     WHERE user.Nam = {[r.Nam]});
                (case uo of
                     None => error <xml>User not found</xml>
                   | Some u =>
                     dml (INSERT INTO instructor (Course, User)
                          VALUES ({[cid]}, {[u]}));
                     ok lv)
            else
                error <xml>You are not authorized to add instructors.</xml>
    in
        lv <- level cid;
        if mayRead lv then
            ok lv
        else
            error <xml>You are not authorized to view this course page</xml>
    end

fun main () =
    u <- User.userId ();
    aa <- amAdmin ();

    case u of
        None => wrap "Welcome" <xml>You must log in to proceed further.</xml>
      | Some u =>
        let
            fun asFoo [fs] [[Course, User] ~ fs] [ks] (desc : string)
                (onCourse : {Course : {Id : int, Nam : string}, T : $fs} -> _)
                (t : sql_table ([Course = course, User = user] ++ fs) ks) : transaction xbody =
                cs <- queryX (SELECT course.Id, course.Nam, t.{{fs}}
                              FROM course, t
                              WHERE course.Id = t.Course
                                AND t.User = {[u]}
                              ORDER BY course.Nam)
                             (fn r => <xml><li>{onCourse r}</li></xml>);

                return <xml>
                  <h3>You are {[desc]}:</h3>

                  {cs}
                </xml>
        in
            asStudent <- asFoo "enrolled as a student in"
                               (fn r =>
                                   let
                                       fun reallyDrop () =
                                           u <- User.userId ();
                                           case u of
                                               None => error <xml>You must be logged in to drop a class.</xml>
                                             | Some u =>
                                               dml (DELETE FROM student
                                                    WHERE Course = {[r.Course.Id]}
                                                      AND User = {[u]});
                                               main ()

                                       fun drop () =
                                           name <- oneRowE1 (SELECT (course.Nam)
                                                             FROM course
                                                             WHERE course.Id = {[r.Course.Id]});
                                           wrap "Really drop?" <xml>
                                             <p>Are you sure you want to drop {[name]}?</p>

                                             <form><submit value="Drop" action={reallyDrop}/></form>
                                           </xml>
                                   in
                                       <xml>
                                         {[r.Course.Nam]}
                                         {case r.T.Grade of
                                              None => <xml/>
                                            | Some g => <xml>(Grade: {[g]})</xml>}
                                         <form><submit value="Drop" action={drop}/></form>
                                       </xml>
                                   end) student;
            asTa <- asFoo "marked as a TA for"
                          (fn r => <xml><a link={courseInfo r.Course.Id}>{[r.Course.Nam]}</a></xml>) ta;
            asInstructor <- asFoo "marked as an instructor for"
                                  (fn r => <xml><a link={courseInfo r.Course.Id}>{[r.Course.Nam]}</a></xml>) instructor;

            allCourses <- (if aa then
                               queryX1 (SELECT *
                                        FROM course
                                        ORDER BY course.Nam)
                                       (fn r => <xml><li><a link={courseInfo r.Id}>{[r.Nam]}</a></li></xml>)
                           else
                               return <xml/>);

            wrap "Welcome" <xml>
              {asStudent}

              {asTa}

              {asInstructor}

              {if aa then
                   <xml>
                     <h3>All courses</h3>

                     {allCourses}

                     <h3>Add course</h3>

                     <form>
                       Name: <textbox{#Nam}/> <submit value="Add" action={addCourse}/>
                     </form>
                   </xml>
               else
                   <xml/>}
            </xml>
        end

and addCourse r =
    aa <- amAdmin ();
    if aa then
        cid <- nextval courseIds;
        dml (INSERT INTO course (Id, Nam)
             VALUES ({[cid]}, {[r.Nam]}));
        main ()
    else
        error <xml>You are not authorized to add courses.</xml>