merge
This commit is contained in:
wadler
commit
8656f2e7af
8 changed files with 243 additions and 96 deletions
2
Makefile
2
Makefile
|
|
@ -1,4 +1,4 @@
|
|||
SHELL := /bin/bash
|
||||
SHELL := /usr/bin/env bash
|
||||
AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
|
||||
AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
|
||||
MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
|
||||
|
|
|
|||
|
|
@ -8,8 +8,9 @@ permalink : /TSPL/2019/
|
|||
|
||||
* **Instructor**
|
||||
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
|
||||
* **Teaching assistant**
|
||||
* **Teaching assistants**
|
||||
- [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
|
||||
- [Orestis Melkonian](mailto:o.melkonian@sms.ed.ac.uk)
|
||||
|
||||
## Lectures
|
||||
|
||||
|
|
|
|||
188
courses/tspl/make_assignment.sh
Executable file
188
courses/tspl/make_assignment.sh
Executable file
|
|
@ -0,0 +1,188 @@
|
|||
#!/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,
|
||||
# making it somewhat specific to courses run there, but the header should be easy to edit.
|
||||
#
|
||||
# Usage:
|
||||
#
|
||||
# ./make_assignment.sh [COURSE_NAME] [COURSE_YEAR] [ASSIGNMENT_NUMBER] [PLFA_SOURCE_FILE...]
|
||||
|
||||
COURSE="$1"
|
||||
shift
|
||||
|
||||
YEAR="$1"
|
||||
shift
|
||||
|
||||
NUM="$1"
|
||||
shift
|
||||
|
||||
## Make assignment header
|
||||
|
||||
cat <<-EOF
|
||||
---
|
||||
title : "Assignment$NUM: $COURSE Assignment $NUM"
|
||||
layout : page
|
||||
permalink : /$COURSE/$YEAR/Assignment$NUM/
|
||||
---
|
||||
|
||||
\`\`\`
|
||||
module Assignment$NUM where
|
||||
\`\`\`
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises labelled "(practice)" are included for those who want extra practice.
|
||||
|
||||
Submit your homework using the "submit" command.
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
|
||||
## Good Scholarly Practice.
|
||||
|
||||
Please remember the University requirement as
|
||||
regards all assessed work. Details about this can be found at:
|
||||
|
||||
> [http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
|
||||
|
||||
Furthermore, you are required to take reasonable measures to protect
|
||||
your assessed work from unauthorised access. For example, if you put
|
||||
any such work on a public repository then you must set access
|
||||
permissions appropriately (generally permitting access only to
|
||||
yourself, or your group in the case of group practicals).
|
||||
|
||||
EOF
|
||||
|
||||
## Awk Scripts
|
||||
|
||||
AWK_GET_IMPORTS='
|
||||
/^#/ {
|
||||
import=0
|
||||
}
|
||||
/^## Imports/ {
|
||||
import=1
|
||||
}
|
||||
/^```/ {
|
||||
code=!code;
|
||||
{
|
||||
if (import)
|
||||
print $0
|
||||
};
|
||||
next
|
||||
}
|
||||
{
|
||||
if (import) {
|
||||
if (code)
|
||||
print " "$0
|
||||
else
|
||||
print $0
|
||||
}
|
||||
}
|
||||
'
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
IFS=$OLDIFS
|
||||
echo " hiding ($HIDING_LIST)"
|
||||
echo '```'
|
||||
echo
|
||||
|
||||
# Extract Exercises
|
||||
awk "$AWK_GET_EXERCISES" "$SRC"
|
||||
done
|
||||
49
courses/tspl/send_marks.sh
Executable file
49
courses/tspl/send_marks.sh
Executable file
|
|
@ -0,0 +1,49 @@
|
|||
#!/usr/bin/env bash
|
||||
|
||||
# Sends out marks for students based on the folder structure used by Submit,
|
||||
# the coursework submission system used in the School of Informatics at the
|
||||
# University of Edinburgh.
|
||||
#
|
||||
# This script assumes the following folder structure:
|
||||
#
|
||||
# $DIR/sXXXXXXX/cw$CW/$FILE
|
||||
#
|
||||
# The variable DIR refers to the directory passed in as an argument to the
|
||||
# script. The variable XXXXXXX refers to the student ID, and it is assumed
|
||||
# that
|
||||
#
|
||||
# sXXXXXXX@sms.ed.ac.uk
|
||||
#
|
||||
# is a valid email address. The variable $CW refers to the number for of the
|
||||
# coursework of which the students are meant to be notified. The directory
|
||||
# DIR/sXXXXXXX/cwY/ should only contain a single file, which should be
|
||||
# specified using the FILE parameter.
|
||||
#
|
||||
# Usage:
|
||||
#
|
||||
# ./send_marks.sh [DIR] [CW] [FILE]
|
||||
|
||||
DIR="$1"
|
||||
shift
|
||||
|
||||
CW="$1"
|
||||
shift
|
||||
|
||||
FILE="$1"
|
||||
shift
|
||||
|
||||
for ATTACHMENT in "${DIR%/}/s"*"/cw$CW/$FILE"; do
|
||||
SUBJ="Mark for coursework $CW"
|
||||
BODY=""
|
||||
SID=$(echo "$ATTACHMENT" | sed 's|.*/\(s[0-9]\{7\}\)/.*|\1|')
|
||||
ADDR="$SID@sms.ed.ac.uk"
|
||||
CMD="echo \"$BODY\" | mail -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\""
|
||||
echo "You are about to run the following command:"
|
||||
echo -e "\n$CMD\n"
|
||||
read -p "Are you sure? " -n 1 -r
|
||||
echo
|
||||
if [[ $REPLY =~ ^[Yy]$ ]]
|
||||
then
|
||||
eval "$CMD"
|
||||
fi
|
||||
done
|
||||
|
|
@ -1,91 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
# 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,
|
||||
# making it somewhat specific to courses run there, but the header should be easy to edit.
|
||||
#
|
||||
# Usage:
|
||||
#
|
||||
# ./make_assignment.sh [COURSE_NAME] [COURSE_YEAR] [ASSIGNMENT_NUMBER] [PLFA_SOURCE_FILE...]
|
||||
|
||||
COURSE="$1"
|
||||
shift
|
||||
|
||||
YEAR="$1"
|
||||
shift
|
||||
|
||||
NUM="$1"
|
||||
shift
|
||||
|
||||
## Make assignment header
|
||||
|
||||
cat <<-EOF
|
||||
---
|
||||
title : "Assignment$NUM: $COURSE Assignment $NUM"
|
||||
layout : page
|
||||
permalink : /$COURSE/$YEAR/Assignment$NUM/
|
||||
---
|
||||
|
||||
\`\`\`
|
||||
module Assignment$NUM where
|
||||
\`\`\`
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises labelled "(practice)" are included for those who want extra practice.
|
||||
|
||||
Submit your homework using the "submit" command.
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
|
||||
## Good Scholarly Practice.
|
||||
|
||||
Please remember the University requirement as
|
||||
regards all assessed work. Details about this can be found at:
|
||||
|
||||
> [http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
|
||||
|
||||
Furthermore, you are required to take reasonable measures to protect
|
||||
your assessed work from unauthorised access. For example, if you put
|
||||
any such work on a public repository then you must set access
|
||||
permissions appropriately (generally permitting access only to
|
||||
yourself, or your group in the case of group practicals).
|
||||
|
||||
EOF
|
||||
|
||||
## Make import statements
|
||||
|
||||
cat <<-EOF
|
||||
|
||||
## Imports
|
||||
|
||||
\`\`\`
|
||||
EOF
|
||||
for SRC in "$@"; do
|
||||
AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"")
|
||||
echo "open import $AGDA_MODULE"
|
||||
done
|
||||
cat <<-EOF
|
||||
\`\`\`
|
||||
|
||||
EOF
|
||||
|
||||
## Extract exercises
|
||||
|
||||
for SRC in "$@"; do
|
||||
NAME=$(basename "${SRC%.lagda.md}")
|
||||
cat <<-EOF
|
||||
|
||||
## $NAME
|
||||
|
||||
EOF
|
||||
awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC"
|
||||
done
|
||||
|
|
@ -656,7 +656,7 @@ Show
|
|||
|
||||
foldr _∷_ [] xs ≡ xs
|
||||
|
||||
Show as a consequence of `foldr-++ above that
|
||||
Show as a consequence of `foldr-++` above that
|
||||
|
||||
xs ++ ys ≡ foldr _∷_ ys xs
|
||||
|
||||
|
|
|
|||
|
|
@ -913,7 +913,7 @@ between the two representations.
|
|||
from : Bin → ℕ
|
||||
|
||||
For the former, choose the bitstring to have no leading zeros if it
|
||||
represents a positive natural, and represent zero by `x0 nil`.
|
||||
represents a positive natural, and represent zero by `⟨⟩ O`.
|
||||
Confirm that these both give the correct answer for zero through four.
|
||||
|
||||
```
|
||||
|
|
|
|||
|
|
@ -169,7 +169,7 @@ checks that the inherited and synthesised types match.
|
|||
|
||||
Similarly, we said above that the function of an application is typed
|
||||
by synthesis and that abstractions are typed by inheritance, giving a
|
||||
mismatch if the function of an application is a variable. Hence, we
|
||||
mismatch if the function of an application is an abstraction. Hence, we
|
||||
need a way to treat an inherited term as if it is synthesised. We
|
||||
introduce a new term form `M ↓ A` for this purpose. The typing
|
||||
judgment returns `A` as the synthesized type of the term as a whole,
|
||||
|
|
|
|||
Loading…
Reference in a new issue