<div dir="ltr"><div dir="ltr">Hi Chris,<div><br></div><div>For "checking static properties at compile time", you may find [sbvPlugin](<a href="https://hackage.haskell.org/package/sbvPlugin">https://hackage.haskell.org/package/sbvPlugin</a>) 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.</div><div><div><br></div><div>Regards,</div><div>Shao Cheng</div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Nov 21, 2018 at 2:47 AM Chris Smith <<a href="mailto:cdsmith@gmail.com">cdsmith@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hey everyone,<div><br></div><div>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.</div><div><br></div><div>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: <a href="https://code.world/haskell#PpwpTF1wv3qIvwhohCfvSrQ" target="_blank">https://code.world/haskell#PpwpTF1wv3qIvwhohCfvSrQ</a></div><div><br></div><div>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.</div><div><br></div><div>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.)</div><div><br></div><div>Has anyone done anything like this before?  Any wisdom to share, or ideas to contribute?</div><div><br></div><div>Thanks,</div><div>Chris</div></div></div></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>