Feedback on plan for checking code requirements in a GHC plugin

Hey everyone, I'm converging on a design for a new feature of CodeWorld, the Haskell-based educational programming environment that I teach with. I'm wondering if anyone has done something like this before. The goal is that when I give an assignment in a class (e.g., "modify this starting code to generalize the repeated pattern using a function"), I want the user to see a checklist of assignment requirements when they run the code. A prototype implementation is here: https://code.world/haskell#PpwpTF1wv3qIvwhohCfvSrQ There are all sorts of possible requirements, such as: "No lines longer than 80 characters", or "there must be a function called foo", or "all top-level definitions must have type signatures", or "your code must define at least 10 top-level variables, and use at least 3 where clauses", or "your definition of var should be equivalent to this one" (see Joachim Breitner's inspection testing work), or even "the function f must satisfy this QuickCheck property". It's been suggested that the requirements language also include the ability to match patterns in the AST, which I think is a good idea. The current prototype uses a pre-compile step that parses the code using haskell-src-exts, and doesn't implement dynamic requirements (runtime-evaluated) at all. My ultimate plan, though, is to send these requirements to GHC via a plugin, then have it evaluate the static ones at compile time, and generate code to check the dynamic ones. Finally, the plugin would add new code to the beginning of main that will invoke a configurable function with the results of the requirement check (hard-coding the static ones, and evaluating dynamic ones on the fly). (In the CodeWorld environment, this function would display the checklist in the web UI, for example.) Has anyone done anything like this before? Any wisdom to share, or ideas to contribute? Thanks, Chris

Hi Chris,
For "checking static properties at compile time", you may find [sbvPlugin](
https://hackage.haskell.org/package/sbvPlugin) useful, it supports
annotating functions with ANN pragmas that declare properties verifiable by
an SMT solver. I haven't used it with ghcjs so not sure if it fits your use
case, but probably worth a try.
Regards,
Shao Cheng
On Wed, Nov 21, 2018 at 2:47 AM Chris Smith
Hey everyone,
I'm converging on a design for a new feature of CodeWorld, the Haskell-based educational programming environment that I teach with. I'm wondering if anyone has done something like this before.
The goal is that when I give an assignment in a class (e.g., "modify this starting code to generalize the repeated pattern using a function"), I want the user to see a checklist of assignment requirements when they run the code. A prototype implementation is here: https://code.world/haskell#PpwpTF1wv3qIvwhohCfvSrQ
There are all sorts of possible requirements, such as: "No lines longer than 80 characters", or "there must be a function called foo", or "all top-level definitions must have type signatures", or "your code must define at least 10 top-level variables, and use at least 3 where clauses", or "your definition of var should be equivalent to this one" (see Joachim Breitner's inspection testing work), or even "the function f must satisfy this QuickCheck property". It's been suggested that the requirements language also include the ability to match patterns in the AST, which I think is a good idea.
The current prototype uses a pre-compile step that parses the code using haskell-src-exts, and doesn't implement dynamic requirements (runtime-evaluated) at all. My ultimate plan, though, is to send these requirements to GHC via a plugin, then have it evaluate the static ones at compile time, and generate code to check the dynamic ones. Finally, the plugin would add new code to the beginning of main that will invoke a configurable function with the results of the requirement check (hard-coding the static ones, and evaluating dynamic ones on the fly). (In the CodeWorld environment, this function would display the checklist in the web UI, for example.)
Has anyone done anything like this before? Any wisdom to share, or ideas to contribute?
Thanks, Chris _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Nothing to add other than this sounds just like the sort of thing that
will be easy to implement as a source plugin.
You might find my plugins resource page useful:
http://mpickering.github.io/plugins.html
In particular, this post about how to construct expressions:
http://mpickering.github.io/posts/2018-06-11-source-plugins.html
Cheers,
Matt
On Tue, Nov 20, 2018 at 6:47 PM Chris Smith
Hey everyone,
I'm converging on a design for a new feature of CodeWorld, the Haskell-based educational programming environment that I teach with. I'm wondering if anyone has done something like this before.
The goal is that when I give an assignment in a class (e.g., "modify this starting code to generalize the repeated pattern using a function"), I want the user to see a checklist of assignment requirements when they run the code. A prototype implementation is here: https://code.world/haskell#PpwpTF1wv3qIvwhohCfvSrQ
There are all sorts of possible requirements, such as: "No lines longer than 80 characters", or "there must be a function called foo", or "all top-level definitions must have type signatures", or "your code must define at least 10 top-level variables, and use at least 3 where clauses", or "your definition of var should be equivalent to this one" (see Joachim Breitner's inspection testing work), or even "the function f must satisfy this QuickCheck property". It's been suggested that the requirements language also include the ability to match patterns in the AST, which I think is a good idea.
The current prototype uses a pre-compile step that parses the code using haskell-src-exts, and doesn't implement dynamic requirements (runtime-evaluated) at all. My ultimate plan, though, is to send these requirements to GHC via a plugin, then have it evaluate the static ones at compile time, and generate code to check the dynamic ones. Finally, the plugin would add new code to the beginning of main that will invoke a configurable function with the results of the requirement check (hard-coding the static ones, and evaluating dynamic ones on the fly). (In the CodeWorld environment, this function would display the checklist in the web UI, for example.)
Has anyone done anything like this before? Any wisdom to share, or ideas to contribute?
Thanks, Chris _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

I'm reviving this old thread, because I am talking to a student who is interested in working on this as a project for Google Summer of Code. I'm happy to be a mentor, but this student could use another mentor who could help with GHC internals for building a GHC plugin. The project would be to implement a domain-specific language for giving assignment or exercise requirements for Haskell programs, and a GHC plugin that allows the code to be run in a mode that validates those requirements. The plugin would inject code into the resulting program for running in validation mode to do the checks. Sometimes, the rules are about the source code -- e.g., "every top-level definition must be accompanied by a type signature", or "no lines longer than 80 characters", or "the program must use a list comprehension" -- in which case the plugin would look at the source code or AST at build time, check assertions about what's there, and inject trivial code to report the result when the program is run. Other times, rules could be about runtime properties or behavior, in which case the injected code would actually run tests to validate the behavior. If anyone is interested in mentoring a student working on this project, please contact me and I'll pass along the info. (I cannot post the student's details publicly, because Summer of Code proposals aren't supposed to be public at this stage, but I can forward responses directly to the student involved.) Thanks, Chris On Wed, Nov 21, 2018 at 12:04 PM Matthew Pickering < matthewtpickering@gmail.com> wrote:
Nothing to add other than this sounds just like the sort of thing that will be easy to implement as a source plugin.
You might find my plugins resource page useful: http://mpickering.github.io/plugins.html
In particular, this post about how to construct expressions: http://mpickering.github.io/posts/2018-06-11-source-plugins.html
Cheers,
Matt On Tue, Nov 20, 2018 at 6:47 PM Chris Smith
wrote: Hey everyone,
I'm converging on a design for a new feature of CodeWorld, the
Haskell-based educational programming environment that I teach with. I'm wondering if anyone has done something like this before.
The goal is that when I give an assignment in a class (e.g., "modify
this starting code to generalize the repeated pattern using a function"), I want the user to see a checklist of assignment requirements when they run the code. A prototype implementation is here: https://code.world/haskell#PpwpTF1wv3qIvwhohCfvSrQ
There are all sorts of possible requirements, such as: "No lines longer
than 80 characters", or "there must be a function called foo", or "all top-level definitions must have type signatures", or "your code must define at least 10 top-level variables, and use at least 3 where clauses", or "your definition of var should be equivalent to this one" (see Joachim Breitner's inspection testing work), or even "the function f must satisfy this QuickCheck property". It's been suggested that the requirements language also include the ability to match patterns in the AST, which I think is a good idea.
The current prototype uses a pre-compile step that parses the code using
haskell-src-exts, and doesn't implement dynamic requirements (runtime-evaluated) at all. My ultimate plan, though, is to send these requirements to GHC via a plugin, then have it evaluate the static ones at compile time, and generate code to check the dynamic ones. Finally, the plugin would add new code to the beginning of main that will invoke a configurable function with the results of the requirement check (hard-coding the static ones, and evaluating dynamic ones on the fly). (In the CodeWorld environment, this function would display the checklist in the web UI, for example.)
Has anyone done anything like this before? Any wisdom to share, or
ideas to contribute?
Thanks, Chris _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
Chris Smith
-
Matthew Pickering
-
Shao Cheng