[Haskell-cafe] Feedback on plan for checking code requirements in a GHC plugin

[Shao Cheng]

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 <cdsmith at gmail.com> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181121/2fde8936/attachment.html>