Imported tutch example

18 files changed, 426 insertions, 0 deletions

diff --git a/examples/autograde-Makefile b/examples/autograde-Makefile
new file mode 120000
index 0000000..82edb24
--- /dev/null
+++ b/examples/autograde-Makefile
@@ -0,0 +1 @@
+../autograde-Makefile
\ No newline at end of file
diff --git a/examples/tutch/.gitignore b/examples/tutch/.gitignore
new file mode 100644
index 0000000..8747365
--- /dev/null
+++ b/examples/tutch/.gitignore
@@ -0,0 +1,2 @@
+grader.*
+.cm/*
diff --git a/examples/tutch/COPYING b/examples/tutch/COPYING
new file mode 100644
index 0000000..c8ca2c9
--- /dev/null
+++ b/examples/tutch/COPYING
@@ -0,0 +1,11 @@
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH
+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,
+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM
+LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR
+OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR
+PERFORMANCE OF THIS SOFTWARE.
diff --git a/examples/tutch/Makefile b/examples/tutch/Makefile
new file mode 100644
index 0000000..c6a5adb
--- /dev/null
+++ b/examples/tutch/Makefile
@@ -0,0 +1,5 @@
+autograde:
+	# h: follow links, i.e., so that we include the contents of the tutch symlink
+	tar chf ../autograde.tar --exclude=./Makefile --exclude=test_handins .
+
+.PHONY: autograde
diff --git a/examples/tutch/checks.sig b/examples/tutch/checks.sig
new file mode 100644
index 0000000..6b0453c
--- /dev/null
+++ b/examples/tutch/checks.sig
@@ -0,0 +1,23 @@
+(* Copyright (C) 2017 Ryan Kavanagh <rkavanagh@cs.cmu.edu>       *)
+(* Distributed under the ISC license, see COPYING for details.   *)
+
+signature CHECKS =
+sig
+    (* checks are either:                                         *)
+    (* Check (name, f):                                           *)
+    (*   f : checks some property, and can catastrophically abort *)
+    (*   or raise some exception if something is not satisfied.   *)
+    (*   Useful for sanity checks like: do all desired files      *)
+    (*   exist?                                                   *)
+    (* Problem (name, f):                                         *)
+    (*   name : must be the same name as the autolab problem      *)
+    (*         that is being graded.                              *)
+    (*   f : returns an integer, which is the score awarded for   *)
+    (*       problem "name".                                      *)
+    datatype checks = Check   of string * (unit -> unit)
+		    | Problem of string * (unit -> real)
+
+    val checks : checks list
+
+    val scoreboard : (string * real) list -> int list option
+end
diff --git a/examples/tutch/checks.sml b/examples/tutch/checks.sml
new file mode 100644
index 0000000..bc0ec3e
--- /dev/null
+++ b/examples/tutch/checks.sml
@@ -0,0 +1,63 @@
+(* Copyright (C) 2017 Ryan Kavanagh <rkavanagh@cs.cmu.edu>       *)
+(* Distributed under the ISC license, see COPYING for details.   *)
+
+(************************************************************)
+(* Make sure you put the tutch sources under support/tutch. *)
+(************************************************************)
+
+functor ChecksHelper (structure H : HELPER) : CHECKS where type checks = H.checks =
+struct
+
+datatype checks = datatype H.checks
+
+(*****************************************************)
+(**********       CONFIGURE ME HERE            *******)
+(*****************************************************)
+
+val tutchPath = "./support/tutch/bin/tutch"
+
+val thePDF = "hw3.pdf"
+
+val requiredFiles = [ thePDF
+		    , "hw3_6a.tut"
+		    , "hw3_6b.tut"
+		    , "hw3_6c.tut" ]
+
+(* Compile tutch *)
+(* Surely one should be able to call CM.make or something... *)
+fun compileTutch () =
+  case H.runCmd "make -C ./support/tutch > /dev/null"
+   of 0 => ()
+    | _ => (H.abortWithMessage o H.stringsInBox)
+	       [ "Unable to compile tutch."
+	       , "Contact course staff." ]
+
+(* Runs tutch on requirements file "req" and tutch file "tut". *)
+(* Awards maxScore if tutch succeeds, 0 otherwise. *)
+fun runTutch req tut maxScore =
+  case H.runCmd (tutchPath ^ " -r " ^ req ^ " " ^ (H.joinHandinPath tut))
+   of 0 => maxScore
+    | _ => let val _ = H.printInBox [ "Tutch thinks something went wrong!"
+				    , "Please fix and try again." ]
+	   in 0.0 end
+
+(* We first make sure all of the required files exist. *)
+(* Then we check that the PDF is a valid PDF. *)
+(* Finally, we grade the tutch problems 6a--6c at 2 points each. *)
+val checks = [ H.Check ("all files present", fn _ => H.checkFilesExist requiredFiles)
+	     , H.Check (thePDF, fn _ => H.checkPDF thePDF)
+	     , H.Check ("tutch compile", fn _ => compileTutch ()) ]
+	     @ (List.map (fn (n,s) =>
+			     H.Problem (n, fn _ => runTutch ("./support/hw3_" ^ n ^ ".req")
+							    ("hw3_" ^ n ^ ".tut")
+							    s))
+			 [("6a", 2.0), ("6b", 2.0), ("6c", 2.0)])
+
+(* Empty scoreboard *)
+fun scoreboard _ = NONE
+
+(*****************************************************)
+(**********        END CONFIGURATION           *******)
+(*****************************************************)
+
+end
diff --git a/examples/tutch/helper.sig b/examples/tutch/helper.sig
new file mode 100644
index 0000000..82467d6
--- /dev/null
+++ b/examples/tutch/helper.sig
@@ -0,0 +1,61 @@
+(* Copyright (C) 2017 Ryan Kavanagh <rkavanagh@cs.cmu.edu>       *)
+(* Distributed under the ISC license, see COPYING for details.   *)
+
+signature HELPER =
+sig
+    datatype checks = Check   of string * (unit -> unit)
+		    | Problem of string * (unit -> real)
+
+    (* Path to the directory under which we can find a student's *)
+    (* submitted files. *)
+    val handinPath : string
+
+    (* Takes in the name of a file submitted by a student *)
+    (* and joins it with handinPath. *)
+    val joinHandinPath : string -> string
+
+    (* Removes handinPath from a path if it prefixes it. *)
+    val stripHandinPath : string -> string
+
+    (* Takes in a list of filenames, and checks if those files *)
+    (* exist in the handinPath directory. *)
+    (* Aborts catastrophically if a file is missing. *)
+    val checkFilesExist : string list -> unit
+
+    (* Uses ghostscript to check if the student submitted a valid *)
+    (* PDF (or an empty file in its place). Aborts catastrophically *)
+    (* if missing. *)
+    val checkPDF : string -> unit
+
+    (* Runs a series of checks and then outputs a list of *)
+    (* (problem name, score) tuples *)
+    val runChecks : checks list -> (string * real) list
+
+    (* Produces an AutoLab JSON score string from a scores list *)
+    (* and optional scoreboard *)
+    val scoresToString : (string * real) list * int list option -> string
+
+    (* Puts a list of strings in a box for printing. *)
+    val stringsInBox : string list -> string list
+
+    (* Prints a list of strings in a box. *)
+    val printInBox : string list -> unit
+
+    (* Prints a string followed by newline. *)
+    val printLn : string -> unit
+
+    (* printLns a list of strings, then the empty score, *)
+    (* then exits. Useful when you need to abort early. *)
+    val abortWithMessage : string list -> 'a
+
+    (* Prints a command and then runs it, returning the exit status *)
+    val runCmd : string -> OS.Process.status
+
+    (* Runs a command (with argument list) using Posix.Process.execp. *)
+    (* Return the program's output as a string, along with its exit status. *)
+    val execpOutput : string * string list -> string * Posix.Process.exit_status
+
+    (* Takes a regex in awk format, and a string, and checks if *)
+    (* the regex matches the string *)
+    val matchesAwkRegex : string * string -> bool
+end
diff --git a/examples/tutch/helper.sml b/examples/tutch/helper.sml
new file mode 100644
index 0000000..d20e96f
--- /dev/null
+++ b/examples/tutch/helper.sml
@@ -0,0 +1,173 @@
+(* Copyright (C) 2017 Ryan Kavanagh <rkavanagh@cs.cmu.edu>       *)
+(* Distributed under the ISC license, see COPYING for details.   *)
+
+functor Helper (structure C : sig val handinPath : string end)
+	:> HELPER =
+struct
+
+exception MissingFile of string
+
+datatype checks = Check   of string * (unit -> unit)
+		| Problem of string * (unit -> real)
+
+val handinPath = C.handinPath
+
+fun printLn s = print (s ^ "\n")
+
+(* Puts strings in boxes... *)
+fun stringsInBox strs =
+  let fun repeatChar c n = String.implode (List.tabulate (n, fn _ => c))
+      val maxLength = List.foldl (fn (s,themax) => Int.max (String.size s, themax)) 0 strs
+      val edge = repeatChar #"#" (maxLength + 4)
+  in
+      edge :: (List.foldr (fn (s,thelist) => ("# "
+					      ^ s
+					      ^ (repeatChar #" " (maxLength - (String.size s)))
+					      ^ " #") :: thelist)
+			  [edge]
+			  strs)
+  end
+
+(* Prints strings in boxes... *)
+fun printInBox strs = List.app printLn (stringsInBox strs)
+
+(* Generates an AutoLab json score string *)
+fun scoresToString (scores, scoreboard) =
+  let val scoreStrings = map (fn (problem, score) => "\"" ^ problem ^ "\": " ^ (Real.toString score)) scores
+      val scores = String.concatWith ", " scoreStrings
+      val scoreboard = case scoreboard
+			of SOME l => ", \"scoreboard\": [" ^ (String.concatWith ", " (map Int.toString l)) ^ "]"
+			 | NONE => ""
+  in
+      "{\"scores\": {" ^ scores ^ "}" ^ scoreboard ^ "}"
+  end
+
+(* Aborts the program by printing strs, and gives an empty score. *)
+fun abortWithMessage strs =
+  let val _ = List.app printLn strs
+      val _ = printLn (scoresToString ([],NONE))
+  in
+      OS.Process.exit OS.Process.success
+  end
+
+
+(* Reads the lines of a file into a list *)
+(* Each string in the file will always be contain a newline (#"\n") at the end. *)
+fun readLines filename =
+  let val inFile = TextIO.openIn filename
+      fun readlines ins =
+	case TextIO.inputLine ins
+	 of SOME ln => ln :: readlines ins
+	  | NONE => []
+      val lines = readlines inFile
+      val _ = TextIO.closeIn inFile
+  in
+      lines
+  end
+
+(* Check if the file exists *)
+fun checkFileExists (name : string) : unit =
+  if OS.FileSys.access (name, [OS.FileSys.A_READ])
+  then ()
+  else raise MissingFile name
+
+fun joinHandinPath file =
+  OS.Path.concat (handinPath, file)
+
+fun stripHandinPath path =
+  if String.isPrefix handinPath path then
+      String.extract (path, String.size handinPath + 1, NONE)
+  else
+      path
+
+
+(* Takes in a list of filenames, and checks if those files *)
+(* exist in the handinPath directory. *)
+(* Exits catastrophically if a file is missing. *)
+fun checkFilesExist filenames =
+  List.app (checkFileExists o joinHandinPath) filenames
+  handle MissingFile name => (abortWithMessage o stringsInBox)
+				 [ "File " ^ (stripHandinPath name) ^ " missing."
+				 , "Please make sure you included all required files and resubmit."]
+
+fun runCmd cmd = (printLn cmd; OS.Process.system cmd)
+
+(* Reads from fd in n byte chunks and treats it all as strings. *)
+fun readAllFDAsString (fd, n) =
+  let val v = Posix.IO.readVec (fd, n)
+  in if Word8Vector.length v = 0 then
+	 ""
+     else
+	 (Byte.bytesToString v) ^ (readAllFDAsString (fd, n))
+  end
+
+(* Runs a command c (command and argument list) using Posix.Process.execp. *)
+(* Return the program's output as a string, along with its exit status. *)
+fun execpOutput (c : string * string list) : string * Posix.Process.exit_status =
+  let val { infd = infd, outfd = outfd } = Posix.IO.pipe ()
+  in case Posix.Process.fork ()
+      of NONE => (* Child *)
+	 (( Posix.IO.close infd
+	  ; Posix.IO.dup2 { old = outfd, new = Posix.FileSys.stdout }
+	  ; Posix.IO.dup2 { old = outfd, new = Posix.FileSys.stderr }
+	  ; Posix.Process.execp c)
+	  handle OS.SysErr (err, _) =>
+		 ( print ("Fatal error in child: " ^ err ^ "\n")
+		 ; OS.Process.exit OS.Process.failure ))
+       | SOME pid => (* Parent *)
+	 let val _ = Posix.IO.close outfd
+	     val (_, status) = Posix.Process.waitpid (Posix.Process.W_CHILD pid, [])
+	     val output = readAllFDAsString (infd, 100)
+	     val _ = Posix.IO.close infd
+	 in (output, status) end
+  end
+
+
+(* Check if a submitted file is a valid PDF using ghostscript. *)
+fun checkPDF pdf =
+  let val spdf = joinHandinPath pdf in
+      case ( runCmd ("gs -o/dev/null -sDEVICE=nullpage " ^ spdf)
+	   , Posix.FileSys.ST.size (Posix.FileSys.stat spdf) )
+       of (_,0) => let val _ = printInBox [ "Warning: The empty file " ^ pdf ^ " is not a valid PDF document."
+					  , "Please make sure to resubmit with a valid PDF document in its place." ]
+		   in () end
+	| (0,_) => ()
+	| _ => (abortWithMessage o stringsInBox)
+		   [ "The file " ^ pdf ^ " is not a valid PDF document."
+		   , "Please resubmit with a valid PDF document (or an empty file) in its place."
+		   , "If you are convinced you submitted a valid PDF, please contact the course staff." ]
+  end
+
+(* Runs all of the checks and grades all of the problems in "checks". *)
+fun runChecks (checks : checks list) =
+  List.foldl (fn (cs,results) =>
+		 case cs
+		  of (Check (n, c)) => let val _ = printLn ("\n\nRunning check " ^ n ^ "...")
+					   val _ = c ()
+					   val _ = printLn " Success.\n"
+				       in results end
+		   | (Problem (n, c)) => let val _ = printLn ("\n\nChecking problem " ^ n ^ "...")
+					     val res = c ()
+					     val _ = printLn (" Score: " ^ (Real.toString res) ^ ".\n")
+					 in (n, res) :: results end)
+	     []
+	     checks
+
+
+(* Returns a score of zero for all problems. *)
+(* Useful when you need to abort but still provide a score. *)
+fun failAll (checks : checks list) =
+  List.foldr (fn (cs,results) =>
+		 case cs
+		  of Problem (n, c) => (n, 0) :: results
+		   | _ => results)
+	     []
+	     checks
+
+structure RE = RegExpFn(structure P = AwkSyntax
+			structure E = ThompsonEngine)
+
+fun matchesAwkRegex (r, s) =
+  let val r = RE.find (RE.compileString r)
+  in Option.isSome (StringCvt.scanString r s) end
+end
diff --git a/examples/tutch/main.sml b/examples/tutch/main.sml
new file mode 100644
index 0000000..95e5bb5
--- /dev/null
+++ b/examples/tutch/main.sml
@@ -0,0 +1,25 @@
+(* Copyright (C) 2017 Ryan Kavanagh <rkavanagh@cs.cmu.edu>       *)
+(* Distributed under the ISC license, see COPYING for details.   *)
+
+structure Main :>
+	  sig
+	      val main : (string * string list) -> OS.Process.status
+	  end
+=
+struct
+structure H = Helper (structure C = struct val handinPath = "handin" end)
+structure C = ChecksHelper(structure H = H)
+
+fun main _ =
+  let val scores = H.runChecks C.checks
+      val scoreboard = C.scoreboard scores
+      (* Make sure the scores are on the last line. *)
+      val _ = print "\n\n\n"
+      (* This below *must must must* be the last thing printed.. *)
+      val _ = H.printLn (H.scoresToString (scores, scoreboard))
+  in OS.Process.success end
+  handle _ => (H.abortWithMessage o H.stringsInBox)
+		  [ "Experienced uncaught exception!"
+		  , "If you believe this to be in error, please contact your"
+		    ^ " course staff." ]
+end
diff --git a/examples/tutch/run.sh b/examples/tutch/run.sh
new file mode 100755
index 0000000..ff313b2
--- /dev/null
+++ b/examples/tutch/run.sh
@@ -0,0 +1,26 @@
+#!/bin/sh
+
+abort () {
+    if [ "x$1" != "x" ]; then
+	echo "$1"
+    fi
+    printf "\n\n{\"scores\": {}}"
+    exit 0
+}
+
+tar -mxf autograde.tar || \
+    abort "Failed to extract autograder."
+
+[ -d handin ] || mkdir handin
+
+[ -f handin.tar ] || \
+    abort "Submission is expected to be at handin.tar. This file does not exist!"
+
+tar -xf handin.tar -C handin || \
+    abort "Failed to extract submission."
+
+ml-build sources.cm Main.main grader || \
+    abort "Failed to compile autograder. Please contact course staff."
+
+sml @SMLload grader.* || \
+    abort "SML autograder exited with error. Please contact course staff."
diff --git a/examples/tutch/sources.cm b/examples/tutch/sources.cm
new file mode 100644
index 0000000..7359047
--- /dev/null
+++ b/examples/tutch/sources.cm
@@ -0,0 +1,9 @@
+Group is
+      $/basis.cm
+      $/regexp-lib.cm
+      support/sources.cm
+      helper.sig (* the HELPER signature *)
+      helper.sml (* the Helper module *)
+      checks.sig (* the CHECKS signature *)
+      checks.sml (* the ChecksHelper functor *)
+      main.sml   (* the big cheese *)
diff --git a/examples/tutch/support/README b/examples/tutch/support/README
new file mode 100644
index 0000000..8c31e1a
--- /dev/null
+++ b/examples/tutch/support/README
@@ -0,0 +1 @@
+Put any support files here.
diff --git a/examples/tutch/support/hw3_6a.req b/examples/tutch/support/hw3_6a.req
new file mode 100644
index 0000000..46dd588
--- /dev/null
+++ b/examples/tutch/support/hw3_6a.req
@@ -0,0 +1 @@
+proof apply : (!x:t.A(x) => B(x)) => (!x:t.A(x)) => (!x:t.B(x));
diff --git a/examples/tutch/support/hw3_6b.req b/examples/tutch/support/hw3_6b.req
new file mode 100644
index 0000000..4598e5b
--- /dev/null
+++ b/examples/tutch/support/hw3_6b.req
@@ -0,0 +1 @@
+proof instance : (!x:t.A(x)) & (?y:t.B(y)) => ?z:t.A(z);
diff --git a/examples/tutch/support/hw3_6c.req b/examples/tutch/support/hw3_6c.req
new file mode 100644
index 0000000..663513c
--- /dev/null
+++ b/examples/tutch/support/hw3_6c.req
@@ -0,0 +1 @@
+proof frobenius : (R & ?x:t.Q(x)) <=> ?x:t.(R & Q(x));
diff --git a/examples/tutch/support/sources.cm b/examples/tutch/support/sources.cm
new file mode 100644
index 0000000..fad8872
--- /dev/null
+++ b/examples/tutch/support/sources.cm
@@ -0,0 +1,2 @@
+(* Add any extra support SML files here *)
+Group is
diff --git a/examples/tutch/test_checks.sh b/examples/tutch/test_checks.sh
new file mode 100755
index 0000000..975ea4c
--- /dev/null
+++ b/examples/tutch/test_checks.sh
@@ -0,0 +1,16 @@
+#!/bin/sh
+
+make -s autograde
+
+for f in test_handins/*.tar; do
+    base=`basename -s .tar ${f}`
+    tmp=`mktemp -d`
+    cp ../autograde.tar ${tmp}
+    cp test_handins/${base}.tar ${tmp}/handin.tar
+    cp ../autograde-Makefile ${tmp}
+    echo "\e[41m!!!!!!! Last 10 output lines for test ${base}:\e[0m"
+    (cd ${tmp}; make -s -f autograde-Makefile | tail -n 10)
+    echo "\e[42m!!!!!!! Expected result:\e[0m"
+    cat test_handins/${base}.exp
+    rm -fr ${tmp}
+done
diff --git a/examples/tutch/test_handins/README b/examples/tutch/test_handins/README
new file mode 100644
index 0000000..b43561b
--- /dev/null
+++ b/examples/tutch/test_handins/README
@@ -0,0 +1,5 @@
+To test your checks.sml, place sample submissions in this directory
+according to the following format:
+
+    somename.tar : the submission you want to test
+    somename.exp : the expected json score