Assignment 4

courses/tspl/2019/tspl2019.md

@@ -54,18 +54,19 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07.
   <td>5</td>
   <td><b>14 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
   <td><b>16 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a></td>
-  <td><b>18 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
+  <td><b>18 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a> and
+                    <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
  </tr>
  <tr>
   <td>6</td>
-  <td><b>21 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
+  <td><b>21 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
-  <td><b>23 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
+  <td><b>23 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
-  <td><b>25 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
+  <td><b>25 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
  </tr>
  <tr>
   <td>7</td>
-  <td><b>28 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
+  <td><b>28 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
-  <td><b>30 Oct</b> (to be decided) </td>
+  <td><b>30 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td> 
   <td><b>1 Nov</b>  (no class) </td>
  </tr>
  <tr>

courses/tspl/make_assignment.sh

@@ -1,5 +1,10 @@
 #!/usr/bin/env bash
 
+# TODO:
+#   - put the exercises from each chapter in their own module
+#   - replicate the imports from that module
+#   - import that module hiding anything defined in an exercise section
+
 # This script can be used to automatically generate assignment files from PLFA source files.
 # It takes a course abbreviation, e.g. TSPL, a year, and the number of the assignment.
 # At the moment, it outputs the University of Edinburgh guidelines for good scholarly practice,
@@ -61,31 +66,123 @@ yourself, or your group in the case of group practicals).
 
 EOF
 
-## Make import statements
+## Awk Scripts
 
-cat <<-EOF
+AWK_GET_IMPORTS='
+    /^#/ {
+        import=0
+    }
+    /^## Imports/ {
+        import=1
+    }
+    /^```/ {
+        code=!code;
+        {
+            if (import)
+                print $0
+        };
+        next
+    }
+    {
+        if (import) {
+            if (code)
+                print "  "$0
+            else
+                print $0
+        }
+    }
+'
 
-## Imports
+AWK_GET_DEFNS='
+    /^#/ {
+        exercise=0
+    }
+    /^#### Exercise/ {
+        exercise=1
+    }
+    /^```/ {
+        code=!code;
+        next
+    }
+    !/^  / {
+        postulate=0
+    }
+    /^postulate/ {
+        postulate=1
+    }
+    /^  [^ :(){}]+ +:/ {
+        if (exercise && code && postulate)
+            print $0
+    }
+    /^[^ :(){}]+ +:/ {
+        if (exercise && code)
+            print $0
+    }
+'
 
-\`\`\`
+AWK_GET_EXERCISES='
-EOF
+    /^#/ {
-for SRC in "$@"; do
+        exercise=0
-    AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"")
+    }
-    echo "open import $AGDA_MODULE"
+    /^#### Exercise/ {
-done
+        exercise=1
-cat <<-EOF
+    }
-\`\`\`
+    /^```/ {
+        code=!code;
+        {
+            if (exercise)
+                print $0
+        };
+        next
+    }
+    {
+        if (exercise) {
+            if (code)
+                print "  "$0
+            else
+                print $0
+        }
+    }
+'
 
-EOF
+## Exercises
-
-## Extract exercises
 
 for SRC in "$@"; do
+
+    # Generate Section & Module Header
     NAME=$(basename "${SRC%.lagda.md}")
-    cat <<-EOF
+    echo
+    echo "## $NAME"
+    echo
+    echo '```'
+    echo "module $NAME where"
+    echo '```'
+    echo
 
-## $NAME
+    # Extract Imports
+    awk "$AWK_GET_IMPORTS" "$SRC"
 
-EOF
+    # Generate Import and Hiding List
-    awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC"
+    echo '```'
+    AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"")
+    echo "  open import $AGDA_MODULE"
+    HIDING_LIST=""
+    OLDIFS=$IFS
+    IFS=$(echo -en "\n\b")
+    for defn in `awk "$AWK_GET_DEFNS" "$SRC"`;
+    do
+        NEW=$(eval "echo \"$defn\" | cut -d: -f1 | xargs")
+        if [ -z "$HIDING_LIST" ]; then
+            HIDING_LIST="$NEW"
+        else
+            HIDING_LIST="$HIDING_LIST; $NEW"
+        fi
+    done
+    IFS=$OLDIFS
+    echo "    hiding ($HIDING_LIST)"
+    echo '```'
+    echo
+
+    # Extract Exercises
+    awk "$AWK_GET_EXERCISES" "$SRC"
 done

src/plfa/part2/DeBruijn.lagda.md

@@ -1375,3 +1375,4 @@ This chapter uses the following unicode:
     ₆  U+2086  SUBSCRIPT SIX (\_6)
     ₇  U+2087  SUBSCRIPT SEVEN (\_7)
     ≠  U+2260  NOT EQUAL TO (\=n)
+

src/plfa/part2/More.lagda.md

@@ -1199,7 +1199,7 @@ _ =
    ∎
 ```
 
-#### Exercise `More` (practice)
+#### Exercise `More` (recommended and practice)
 
 Formalise the remaining constructs defined in this chapter.
 Make your changes in this file.
@@ -1207,10 +1207,15 @@ Evaluate each example, applied to data as needed,
 to confirm it returns the expected answer:
 
   * sums (recommended)
-  * unit type
+  * unit type (practice)
-  * an alternative formulation of unit type
+  * an alternative formulation of unit type (practice)
   * empty type (recommended)
-  * lists
+  * lists (practice)
+
+Please delimit any code you add as follows:
+
+    -- begin
+    -- end
 
 
 #### Exercise `double-subst` (stretch)