Update the docs and improve the proof library.

doc/en/Authoring/Parsons.md

@@ -31,7 +31,6 @@ Assume the question author writes a list of strings in Maxima, `proof_steps` in
 
 or they can avoid strings going via Maimxa at all by writing JSON directly
 
-
 Both these approaches can be combined
 
 ````
@@ -94,6 +93,26 @@ The default options are TODO: confirm the above syntax and the default options!
 2. The applet returns up updated state (indentical format: maxima expression) for evaluation by a PRT.  This is linked to an input with parameter `input=`.
 3. `height` and `width` paramaters exist.  TODO: examples/specs.
 
+## Random generation of `proof_step` order
+
+To track which random variants of a question a student sees, and make sure they return to the same varient, we need to perform all randomisation at the Maxima level.
+
+You must define steps as Maxima objects using a `proof_steps` list (see the documentation of for [CAS libraries for representing text-based proofs](../Proof/Proof_CAS_libraries.md)) then you can randomly order the `proof_steps` as follows.
+
+1. Define `proof_steps` as normal.
+2. Add in `proof_steps:random_permutation(proof_steps);` to the question variables.
+3. Add in a question note `{@map(first, proof_steps)@}` to create a meaningful, minimal, question note giving the order of steps.
+
+Note, if you randomly generate random variants it is _strongly recommended_ you use text-based keys.  Keeping track of permuted numerical keys will be impossible!
+
+## Block connection with Maxima
+
+All communication to and from the Parsons block uses the JSON format.  However, internally STACK uses maxima objets.  We therefore need to convert between Maxima syntax and JSON format.
+
+1. The maxima function `stackjson_stringify(proof_steps)` will convert a list of `proof_steps` into a JSON string.
+2. The maxima function `proof_parsons_interpret(ans1)` will convert a JSON string into a [proof construction function](../Proof/Proof_CAS_library.md).
+3. The maxima function `proof_parsons_key_json(ta, proof_steps)` takes the teacher's answer `ta` and a list of proof steps `proof_steps` and creates a JSON string which represents `ta` and lists any available (unused) strings from the `proof_steps` list.  This function is needed to set up the "model answer" field in the inputs from a maxima representation of the proof.
+
 ### Block paramaters: `height` and `width`
 
 Additional display options including `height` and `width` may also be passed to the header, as in 
@@ -113,8 +132,6 @@ Additional display options including `height` and `width` may also be passed to
 
 ## Adding plots to a Parson's block
 
-TODO: confirm if we can embed HTML.  If so, then the following should work.
-
 Since HTML can be embedded into strings dragged within a Parson's block, images can be included with the HTML `<img>` tags as normal.
 
 STACK-generated [plots](../Plots/index.md) cannot be included just using `{@plot(x^2,[x,-1,1])@}` as might be expected.  This is because of the _order_ of evaluation.  The full URL of the image is only created in the (complex) chain of events after the value has been substituted into the Javascript code. Instead, to embed STACK-generated images evaluate a static string using the Maxima `castext` function, and then use the value of `s1` in the Parson's block.  For example.

doc/en/Proof/Proof_CAS_library.md

@@ -60,8 +60,9 @@ Note that the variable `proof_steps` is a _list_ of lists:  `[ ["key", "step", (
   * Using keys: `proof_iff(proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd"),proof("contrapos","assnotodd","even","alg_even","def_M_even","conc_even"))`
 3. The `proof_steps` list can contain an optional string argument `"comment"`.  This string can be used to store justification, explaination and narative.  Only some display functions use this argument, when it exists.
 4. Note that the backslash must be protected when defining these strings.
+5. The strings can contain HTML, including `<img>` tags for inclusing images within draggable elements.
 
-`proof_steps_sub(ex, proof_steps)` takes a proof built from numbered indexes, and translate this into string keys.  In the above example, it might be easier to author a proof as `proof(1,2,3,4,5)` rather than type in `proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd")`. The whole design could be built on numbered keys (and these are valid), but string keys are easier to remember and easier to interpret when looking at students' attempts.  Also, string keys can be inserted later without the need to re-number existing numerical keys.
+`proof_keys_sub(ex, proof_steps)` takes a proof built from numbered indexes, and translate this into string keys.  In the above example, it might be easier to author a proof as `proof(1,2,3,4,5)` rather than type in `proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd")`. The whole design could be built on numbered keys (and these are valid), but string keys are easier to remember and easier to interpret when looking at students' attempts.  Also, string keys can be inserted later without the need to re-number existing numerical keys. Do not use numerical keys if you intend to randomly permute the strings in the proof!
 
 `proof_getstep(key, proof_steps)` looks for the key `key` in the `proof_steps` list.  They key can be either a numerical, or string key.  If found then the function returns the full string, otherwise the key is returned without an error.  One advantage of this approach is that the teacher can define abreviated, alternative proofs using some of the strings in `proof_steps`, e.g. using the above example the following omits all the detail in the sub-proofs, focusing on the structure and hypothesis/conclusion of each block.
 

doc/en/Topics/Parsons.md

@@ -23,6 +23,8 @@ We might expect/require two conscious and separate blocks
 
 The order in which these two sub-proofs are presented is (normally) irrelevant.  That is the _if and only if_ proof construct allows its two sub-proofs to commute.  This is precisely the same sense in which \(A=B\) and \(B=A\) are equivalent. There are _blocks_ within the proof which can change order. Furthermore, since proofs are often nested blocks these sub-proofs may themselves have acceptable options for correctness.
 
+STACK provides "proof construction functions" with arguments. For example, an if and only if proof would be represented as `proof_iff(A,B)`.
+
 Proofs often contain local variables.  Use of explicit block-structres clarify the local scope of variables, and the local scope of assumptions.
 
 If the student has an opportunity to indicate more structure, then the assessment logic becomes considerably simpler, more reliable and transparent. Actually, we think there is significant educational merit in making this structure explicit and consciously separating proof-structure from the finer grained details. It is true that professional mathematicians often omit indicating explicit structure, they abbreviate and omit whole blocks ("the other cases are similar") but these are all further examples of expert reversal.
@@ -32,9 +34,10 @@ Notes
 * Lists are a special case of a tree with one root (the list creation function) and an arbitrary number of nodes in order.  Hence our design explicitly includes traditional Parson's problems as a special case.
 * Teachers who do not want to scaffold explicit block structures (e.g. signal types of proof blocks) can choose to restrict students to (i) flat lists, or (ii) lists of lists.
 
-# Minimal Parson's question
+# Example 1: a minimal Parson's question
 
 The following is a minimal Parson's question where there student is expected to create a list in one and only one order.
+It shows the proof that _\(\log_2(3)\) is irrational_.
 
 ## Question variables
 
@@ -47,9 +50,11 @@ ta:proof("assume","defn_rat","defn_rat2","defn_log","defn_log2","alg","alg_int",
 
 The optional library `prooflib.mac` contain many useful functions for dealing with student's answers which represent proofs.
 
+The variable `ta` holds the teacher's answer which is a proof construction function `proof`.  The arguments to this function are string keys, e.g. `"alg"` which refer to lines in the proof.  The teacher expects these lines in this order.
+
 ## Question text
 
-The example question text below contains a Parson's block. Within the header of the Parson's block, ensure that `input="inputvar"` is included, where `inputvar` is the identifier of the input, for example `input="ans1"` as below. A minimal working example for the proof that _\(\log_2(3)\) is irrational_ is achieved by placing the following in the _Question text_ field:
+The example question text below contains a Parson's block. Within the header of the Parson's block, ensure that `input="ans1"` is included, where `ans1` is the identifier of the input. Place the following in the _Question text_ field:
 
 ````
 <p>Show that \(\log_2(3)\) is irrational. </p>
@@ -71,15 +76,16 @@ The example question text below contains a Parson's block. Within the header of
 
 Notes:
 
-1. The Parson's block requires a JSON object containins `"key":"string"` pairs. The `string` will be shown to the student.  The student's answer will be returned in terms of the `key` tags.  Numbers can be used as keys, but names keys above will be more specific.
+1. The Parson's block requires a JSON object containins `"key":"string"` pairs. The `string` will be shown to the student.  The student's answer will be returned in terms of the `key` tags.  Numbers can be used as keys, but named keys above will be more specific.  We strongly recommend using named keys.
 2. The `\` character in the string must be protected!  Notice that `\(...\)` needs to be typed as `\\(...\\)`.
 3. The [Parson's block](../Authoring/Parsons.md) has a wide range of options such as `height` and `width` which are documented elsewhere.
 
 ## Input: ans1
 
 1. The _Input type_ field should be **String**. 
-2. The _Model answer_ field should be initially empty, i.e. `""`
+2. The _Model answer_ field should construct a JSON object from the teacher's answer `ta` using `proof_parsons_key_json(ta, [])`.  You can replace the empty list in the second argument with a `proof_steps` list if you want to display unused steps as well.  (How to construct and use a `proof_steps` list will be documented below.)
 3. Set the option "Student must verify" to "no".
+4. Set the extra options to "hideanswer" to make sure the JSON representation of the teacher's answer is not shown to the student later as an answer.
 
 ## Potential response tree: prt1
 
@@ -89,19 +95,18 @@ Define the feedback variables:
 sa:proof_parsons_interpret(ans1);
 ````
 
-The student's answer will be a _JSON string_, but we need to interpret which of the strings have been used and in what order.  The `proof_parsons_interpret` takes a JSON string and  builds a proof representation object.
+The student's answer will be a _JSON string_, but we need to interpret which of the strings have been used and in what order.  The `proof_parsons_interpret` function takes a JSON string and  builds a proof representation object.
 
 Then you can set up the potential response tree to be `ATAlgEquiv(sa,ta)` to confirm the student's answer is the same as the teacher's answer.
 
-# Parson's question with block order options
+# Example question 2: a proof with interchangable block order
 
 The following Parson's question is an _if and only if_ proof, containing two blocks in order.
 
 The input is unchanged from the above example. For the question variables use
 
 ````
 stack_include("contribl://prooflib.mac");
-dispproof_para([ex]) := block([ex1],apply(sconcat, flatten(append(["<p>"], [simplode(ex, " ")], ["</p>"]))));
 
 ta:proof_iff(proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd"), proof("contrapos","assnotodd","even","alg_even","def_M_even","conc_even"));
 
@@ -158,11 +163,11 @@ To see this in action, try the following in the general feedback to display both
 
 ````
 This is the proof, written with some structure
-{@ev(tad[1], map(lambda([ex], ex=dispproof), proof_types))@}
+{@proof_display(tad[2], proof_steps)@}
 Notice this proof has two sub-proofs, which can occur in any order.  Therefore we have two correct versions of this proof.
 <table><tr>
-<td><div class="proof">{@ev(tad[1], map(lambda([ex], ex=dispproof_para), proof_types))@}</div></td>
-<td><div class="proof">{@ev(tad[2], map(lambda([ex], ex=dispproof_para), proof_types))@}</div></td>
+<td><div class="proof">{@proof_display_para(tad[1], proof_steps)@}</div></td>
+<td><div class="proof">{@proof_display_para(tad[2], proof_steps)@}</div></td>
 </tr></table>
 Can you see the differences between these proofs?
 ````
@@ -171,3 +176,22 @@ Can you see the differences between these proofs?
 
 You should hide the inputs from students with CSS after testing, e.g. `<p style="display:none">...</p>`.
 
+Note that all connection between the Parson's block and a string input is JSON format.  Therefore input `ans1` is a string, and we convert to and from JSON at various places in the process.
+
+It is likely you will want to randomly permute the strings in the `proof_steps` list before the student sees them.  This is documented in the [Parson's block reference documentation](../Authoring/Parsons.md).
+
+## "The teacher's answer is"....
+
+The design of the interaction between the Parson's block and a STACK input is through JSON.  This raw JSON will not be meaningful to students, hence the suggestion to hide the inputs from students with CSS after testing, e.g. `<p style="display:none">...</p>`.
+
+We recommend the string input holding the JSON does not get shown to the student as a "correct answer". Set the extra options to "hideanswer" in the input to stop this input being displayed.
+
+To display a correct proof as a "teacher's answer"
+
+1. Create a new input `ans2`.
+2. The _Input type_ field should be **String**. 
+3. The _Model answer_ field should display the correct proof constructed from a proof construction functions `ta` and a list of proof steps `proof_steps`.  Set the model answer to `proof_display(ta, proof_steps)`.  You can choose any of the other display functions in the [CAS libraries for representing text-based proofs](../Proof/Proof_CAS_library.md).
+4. Set the option "Student must verify" to "no".
+5. Hide this input with CSS `<p style="display:none">...</p>`.
+
+This input is not used in any PRT.

stack/maxima/assessment.mac

@@ -199,6 +199,12 @@ removeonce(ex, l) := block(
   append([first(l)], removeonce(ex,rest(l)))
 )$
 
+/* All the elements of l1, which do not occur in l2.  Removes all occurances from l1, not one at a time. */
+listdifference(l1, l2) := block(
+  if emptyp(l1) or emptyp(l2) then return(l1),
+  listdifference(sublist(l1, lambda([ex], not(ev(is(ex=first(l2)), simp)))), rest(l2))
+);
+
 /* Remove any common elements from [l1,l2], with duplication. */
 list_cancel(ex) := block([l1, l2, l3],
   l1:first(ex),

stack/maxima/contrib/prooflib.mac

@@ -199,6 +199,26 @@ proof_parsons_interpret(st) := block([pf],
 );
 s_test_case(proof_parsons_interpret("{\"used\":[\"0\",\"3\",\"5\"],\"available\":[\"1\",\"2\",\"4\",\"6\",\"7\"]}"), proof("0","3","5"));
 
+/*
+ * Takes a proof, and proof steps list and returns the keys not used in the proof_steps.
+ * Needed to create a "teacher's answer" in JSON block, including unused text.
+*/
+proof_parsons_keys_used_unused(proof_ans, proof_steps) := block([tkeys, skeys],
+  tkeys:map(first, proof_steps),
+  skeys:ev(proof_ans, map(lambda([ex], ex="["), proof_types), simp),
+  /* TODO: update this when we deal with trees (and have examples) */
+  skeys:flatten(skeys),
+  return([skeys, listdifference(tkeys, ev(unique(skeys), simp))])
+);
+
+/* Construct the "used" and "available" keys when the teacher's answer is used. */
+proof_parsons_key_json(proof_ans, proof_steps) := block([pkeys],
+  /* Ensure all keys are string keys. */
+  if not(emptyp(proof_steps)) then proof_ans:proof_keys_sub(proof_ans, proof_steps),
+  pkeys:proof_parsons_keys_used_unused(proof_ans, proof_steps),
+  sconcat("{\"used\":", stackjson_stringify(first(pkeys)), ", \"available\":", stackjson_stringify(second(pkeys)), "}")
+);
+
 /******************************************************************/
 /*                                                                */
 /*  Display functions                                             */
@@ -231,9 +251,10 @@ proof_disp_replacesteps(ex, proof_steps) := block(
  * Take a proof "ex" and a list "pf" of [key, step] pairs and translate this into a proof tree with
  * the keys replaced by corresponding strings.
  */
-proof_steps_sub(ex, pf):= block(
+proof_keys_sub(ex, proof_steps):= block(
    if integerp(ex) then return(first(proof_steps[ex])),
-   apply(op(ex), map(lambda([ex2], proof_steps_sub(ex2, pf)), args(ex)))
+   if stringp(ex) then return(ex),
+   apply(op(ex), map(lambda([ex2], proof_keys_sub(ex2, proof_steps)), args(ex)))
 );
 
 /**
@@ -253,8 +274,6 @@ dispproof([ex]) := block([ex1],
     apply(sconcat, flatten(append(["<div class=\"proof-block\">"], [simplode(ex, "<br/>")], ["</div>"])))
 );
 
-
-
 /**
  * Take a proof, and any proof steps and display them using proof CSS.
  */