Update make_assignment script to place exercises from each chapter in their own module, import the chapter and its dependencies, hiding duplicate definitions.

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='
+    /^#/ {
+        exercise=0
+    }
+    /^#### Exercise/ {
+        exercise=1
+    }
+    /^```/ {
+        code=!code;
+        {
+            if (exercise)
+                print $0
+        };
+        next
+    }
+    {
+        if (exercise) {
+            if (code)
+                print "  "$0
+            else
+                print $0
+        }
+    }
+'
+
+## Exercises
 
-\`\`\`
-EOF
 for SRC in "$@"; do
+
+    # Generate Section & Module Header
+    NAME=$(basename "${SRC%.lagda.md}")
+    echo
+    echo "## $NAME"
+    echo
+    echo '```'
+    echo "module $NAME where"
+    echo '```'
+    echo
+
+    # Extract Imports
+    awk "$AWK_GET_IMPORTS" "$SRC"
+
+    # Generate Import and Hiding List
+    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
-cat <<-EOF
+    IFS=$OLDIFS
-\`\`\`
+    echo "    hiding ($HIDING_LIST)"
+    echo '```'
+    echo
 
-EOF
+    # Extract Exercises
-
+    awk "$AWK_GET_EXERCISES" "$SRC"
-## Extract exercises
-
-for SRC in "$@"; do
-    NAME=$(basename "${SRC%.lagda.md}")
-    cat <<-EOF
-
-## $NAME
-
-EOF
-    awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC"
 done