stable format for import and export

src/editpage/components/blocks/WpBlock.vue

@@ -50,7 +50,22 @@ export default {
       });
       // Replace coqdoc-style lists (-) with markdown lists (*)
       converted = converted.replace(/^([ ]*)- /gm, '$1* ');
-      return md.render(converted);
+      // Remove coq-comment start & end
+      converted = converted.replace(/\(\*/g, '(💧');
+      converted = converted.replace(/\*\)/g, '💧)');
+      // Translate code
+      converted = converted.replace(/\[\[/g, '```');
+      converted = converted.replace(/\]\]/g, '```');
+      converted = converted.replace(/\[/g, '`');
+      converted = converted.replace(/\]/g, '`');
+      // Translate bold to md
+      converted = converted.replace(/#<\/?strong>#/g, '**');
+      // Translate italics to md
+      converted = converted.replace(/\W_/g, ' *');
+      converted = converted.replace(/_\W/g, '* ');
+
+      converted = md.render(converted);
+      return converted;
     },
     renderToSpan: function(text) {
       let htmlString = this.render(text);

src/io/compileToVO.js

@@ -5,7 +5,7 @@ const util = require('util');
 const execFile = util.promisify(require('child_process').execFile);
 import {getAppdataPath, getResourcesPath} from './pathHelper';
 import read, {deleteFile, doesFileExist, readFile} from './readfile';
-import {blockToCoqText} from './notebook';
+import {wpToCoq} from './notebook';
 
 const extensions = ['wpn', 'v', 'vo'];
 
@@ -105,7 +105,7 @@ class VOCompiler {
       return;
     }
     const notebook = await readFile(filepath);
-    const text = blockToCoqText(notebook.blocks);
+    const text = wpToCoq(notebook.blocks);
 
     return new Promise((resolve, reject) => {
       fs.writeFile(filepath.substring(0, filepath.length - 3) + 'v', text,

src/io/notebook.js

@@ -1,10 +1,6 @@
-const fs = require('fs');
+import {assert} from 'console';
 
-const COQ_COMMENT_START = '(*';
-const COQ_SPECIAL_COMMENT_START = '(** ';
-const COQ_COMMENT_END = '*)';
-const COQ_INPUT_START = '(* Start of input area *)';
-const COQ_INPUT_END = '(* End of input area *)';
+const fs = require('fs');
 
 const DEFAULT_BLACKLIST = [
   // commands that allow introducing theorems without proof
@@ -275,7 +271,7 @@ class Notebook {
    * @return {String} text that will be displayed
    */
   parseToText(hints = true, textblocks = true, coqcode = true) {
-    return blockToCoqText(this.blocks);
+    return wpToCoq(this.blocks);
   }
 
   /**
@@ -343,6 +339,7 @@ class Notebook {
       }
 
       try {
+        // TODO move this to seperate function, also for coqToWp?
         this.clearContent();
         const read = JSON.parse(data);
 
@@ -503,13 +500,14 @@ class Notebook {
           this.createCodeBlock(coqText),
         ];
       } else {
-        this.blocks = this.coqToCodeAndText(coqText);
+        this.blocks = coqToWp(coqText);
       }
     };
 
     fs.readFile(filename, callback);
   }
 
+  // TODO: unused function, perhaps in future when WP docs are one big doc.
   /**
    * Cuts a string up in an array of strings. The cut points are
    * exactly at the beginning of the matches of the regular expression keywords
@@ -535,88 +533,146 @@ class Notebook {
 
     return stringPieces;
   }
+}
 
-  /**
-   * Converts coq code to a notebook format
-   * This does not convert back any waterproof things and just puts all
-   * special comments in text blocks and the rest in code blocks.
-   * @param {String} coqCode the input code
-   * @return {Array} the blocks from the code
-   */
-  coqToCodeAndText(coqCode) {
-    const blocks = [];
-    let contentLeft = coqCode.replace(/\r/g, '');
-    while (contentLeft.length > 0) {
-      let nextComment = contentLeft.indexOf(COQ_SPECIAL_COMMENT_START);
-
-      if (nextComment < 0 || nextComment > 0) {
-        const codeBeforeComment = nextComment >= 0 ?
-            contentLeft.substring(0, nextComment) : contentLeft;
-        const codePieces =
-            this.cutStringBetweenKeywords(codeBeforeComment.trim());
-        for (let i = 0; i < codePieces.length; i++) {
-          blocks.push(this.createCodeBlock(codePieces[i]));
-        }
-        if (nextComment < 0) {
-          break;
-        }
-      }
-
-      contentLeft = contentLeft.substring(nextComment)
-          .replace(COQ_SPECIAL_COMMENT_START, '');
-
-      let startPos = 0;
-      let endPos = 0;
-      nextComment = contentLeft.indexOf(COQ_COMMENT_START, startPos);
-      let commentEnd = contentLeft.indexOf(COQ_COMMENT_END, endPos);
-
-      while (commentEnd >= 0 && nextComment >=0 && nextComment < commentEnd) {
-        startPos = nextComment + 2;
-        endPos = commentEnd + 2;
-        nextComment = contentLeft.indexOf(COQ_COMMENT_START, startPos);
-        commentEnd = contentLeft.indexOf(COQ_COMMENT_END, endPos);
-      }
+export default Notebook;
 
-      if (commentEnd < 0) {
-        blocks.push(this.createTextBlock(contentLeft));
-        break;
+/**
+ * Importing from .v file according to specification.md
+ * @param {String} coqCode the input code
+ * @return {Array} the blocks from the code
+ */
+function coqToWp(coqCode) {
+  const blocks = []; // return array
+  let inInputField = false;
+  let inputFieldId = 1;
+  let i = 0;
+  while (i < coqCode.length) {
+    let next = coqCode.indexOf('(**', i+3);
+    if (next === -1) {
+      next = coqCode.length;
+    }
+    const blockContent = coqCode.substring(i, next).trim();
+    const finalCommentCloseIndex = blockContent.lastIndexOf('*)');
+    if (finalCommentCloseIndex !== -1) {
+      const coqdoc = blockContent.substring(3, finalCommentCloseIndex).trim();
+      if (coqdoc === '') {
+        // The block could have been (***) or an empty text block. We don't add
+        // a block in that case.
+      } else {
+        const block = {};
+        if (coqdoc === 'INPUT-START') {
+          // FIXME: Open input blocks get closed before a next input
+          // block is opened, additional closures of input blocks are ignored
+          assert(
+              inInputField === false,
+              'INPUT-START encountered, but input section has already started.'
+          );
+          block.type = 'input';
+          block.start = true;
+          block.id = 'input-' + inputFieldId;
+          inInputField = true;
+        } else if (coqdoc === 'INPUT-END') {
+          assert(
+              inInputField === true,
+              'INPUT-END encountered, but not in an input section.'
+          );
+          block.type = 'input';
+          block.start = false;
+          block.id = 'input-' + inputFieldId;
+          inInputField = false;
+          inputFieldId++;
+        } else if (coqdoc.indexOf('<hint>') !== -1) {
+          block.type = 'hint';
+          block.text = coqdoc;
+        } else {
+          block.type = 'text';
+          block.text = coqdoc;
+        }
+        const withinInputFieldMarkers = inInputField && block.type !== 'input';
+        Notebook.setDefaultBlockState(block, withinInputFieldMarkers);
+        blocks.push(block);
       }
-
-      blocks.push(this.createTextBlock(contentLeft.substring(0, commentEnd)));
-      contentLeft = contentLeft.substring(commentEnd)
-          .replace(COQ_COMMENT_END, '');
     }
-
-    return blocks;
+    let startCode;
+    if (finalCommentCloseIndex === -1) {
+      startCode = 0;
+    } else {
+      startCode = finalCommentCloseIndex + 2;
+    }
+    const code = blockContent.substring(startCode).trim();
+    if (code !== '') {
+      const block = {type: 'code', text: code};
+      Notebook.setDefaultBlockState(block, inInputField);
+      blocks.push(block);
+    }
+    i = next;
   }
+  return blocks;
 }
 
-export default Notebook;
-
 /**
- * Convert blocks into a coq parsable text
+ * Exporting to .v file according to specification.md
  * @param {[]} blocks the list of blocks
- * @return {string} the coq valid text
+ * @return {string} the coq text
  */
-function blockToCoqText(blocks) {
-  let coqContent = '';
+function wpToCoq(blocks) {
+  const blockStrings = [];
+  let prevBlockType = null;
   for (const block of blocks) {
     if (block.type === 'code') {
-      coqContent += block.text;
+      if (prevBlockType === 'code') {
+        blockStrings.push('(***)');
+      }
+      blockStrings.push(block.text);
+    } else if (block.type === 'text') {
+      blockStrings.push('(** ' + convertToValid(block.text) + ' *)');
+    } else if (block.type === 'hint') {
+      const hint = block.text.split('<hint>');
+      if (hint.length == 2) {
+        blockStrings.push(
+            '(** ' + convertToValid(hint[0].trim()) + '\n<hint>\n'
+            + convertToValid(hint[1].trim()) + ' *)'
+        );
+      } else {
+        throw Error('Unexpected hint block: ' + hint.text);
+      }
     } else if (block.type === 'input') {
       if (block.start) {
-        coqContent += COQ_SPECIAL_COMMENT_START + COQ_INPUT_START
-          + COQ_COMMENT_END;
+        blockStrings.push('(** INPUT-START *)');
       } else {
-        coqContent += COQ_SPECIAL_COMMENT_START + COQ_INPUT_END
-          + COQ_COMMENT_END;
+        blockStrings.push('(** INPUT-END *)');
       }
     } else {
-      coqContent += COQ_SPECIAL_COMMENT_START + block.text + COQ_COMMENT_END;
+      throw Error('Can not interpret block type ' + block.type);
     }
-    coqContent += '\n';
+
+    prevBlockType = block.type;
   }
-  return coqContent;
+  return blockStrings.join('\n');
+}
+
+/**
+ * Convert a block's text to something that is valid.
+ * @param {string} text
+ * @return {string} converted text
+ */
+function convertToValid(text) {
+  // Close string literal
+  let converted = text;
+
+  // Close all open comments
+  // Open comments at the beginning
+  const opens = (converted.match(/\(\*/g) || []).length;
+  const closes = (converted.match(/\*\)/g) || []).length;
+  if (opens > closes) {
+    converted = converted + ' *)' * (opens - closes);
+  } else if (closes > opens) {
+    converted = (closes - opens) * '(* ' + converted;
+  }
+  // Seperate setting for doubling $, %, #
+
+  return converted;
 }
 
-export {blockToCoqText, COQ_SPECIAL_COMMENT_START};
+export {coqToWp, wpToCoq};

src/io/specification.md

@@ -0,0 +1,98 @@
+# Importing/exporting waterproof notebooks from/to vernacular file
+We aim to make the exported .v files easy to read, and adhering to coqdoc format for nice coqdoc rendering. We are a bit constrained as we like *exact reproducibility*, though we will settle for approximate reproducibility for the benefit of readability of .v files.
+
+## Waterproof notebooks and exercise sheets
+
+Waterproof notebooks and exercise sheets are practically `.json` files, but have extensions `.wpn` and `.wpe` respectively. The files have two attributes, `exerciseSheet` and `blocks`. For a notebook, `exerciseSheet : false` and for an exercise sheet, `exerciseSheet : true`. 
+The blocks attribute is a sequence of dictionaries. Every element in the sequence contains:
+
+- a field `type`, which is one of: `text`, `code`, `input` or `hint`.
+- a field `text`, which contains the content of the block
+- a field `id`, which is present if and only if the field is an input block, which contains a unique identifier for the block
+- a field `start`, which is present if and only if the field is an input block, which encodes whether this is the start or the end of an input block
+
+## Exporting to `.v` file
+
+We export a notebook or exercisesheet to a `.v` file as follows:
+
+- If it is a code block: simply return the content stored in the field `text`. Between the output of two consecutive code blocks, we add `(***)`.
+- If it is a text block: return `(** convert_to_valid(text) *)`.
+- If it is a hint block: return `(** convert_to_valid(text_before_first_<hint>)\n<hint>\nconvert_to_valid(text_after_first_<hint>)*)`.
+- If it is an input block:
+   - with `start == True`: return `(** INPUT-START *)`
+   - with `start == False`: return `(** INPUT-END *)` **We could get away with only writing INPUT and inferring whether it is start or end, but this is more informative in .v files in my opinion**
+- Make (separate) settings whether $, %, and/or # occurring in hint or text blocks need to be doubled on export
+
+For re-importing, everything we encounter that is not in a `(**` and `*)` is a code block. Originally contiguous code blocks will become one large code blocks. To split these up, you can input an empty text block `(** *)` or even `(***)` (the latter is not rendered in coqdoc, while the former is rendered as an empty line).
+
+## Importing to `.v` file
+
+- The (outer-layer) coqdoc comments `(** INPUT-START *)` and `(** INPUT-END *)` are mapped to blocks with type `input`
+- Outer-layer coqdoc comments that somewhere contain `<hint>` are converted to hint blocks.
+- Every other outmost-layer coqdoc comment gets assigned an input block type `text` with contents of the coqdoc comment.
+- The `id` of the `n`th imported input block is assigned `input-n`
+- Open input blocks get closed before a next input block is opened, additional closures of input blocks are ignored
+- If no text is present before `<hint>` in open hint block, then add standard text: Click to open hint.
+- Note: text is not stripped
+- Make (separate) settings whether $, %, and/or # occurring in hint or text blocks need to be halved on import
+
+## Conversion to valid text
+
+Decision/aim: stay as close as possible to coqdoc notation in the json file. Only in rendering go to the markdown dialect.
+
+The function `convert_to_valid` performs the following actions:
+
+- Close string literal at the end of the markdown block (if one is open at the end)
+- Close all open comments at the end of the markdown block
+- Open comments at the beginning of the markdown block
+
+### Waterproof conversions:
+
+Convert in rendering (in the `render` function in `WpBlock.vue`)
+
+- `(*` to `(💧` and `*)` to `💧)`, where precedence goes from left to right.
+- Header-*'s to #'s
+- `#<strong>#` and `#</strong>#` both to `**`
+- Consecutive `[[` and `]]` both to triple backticks. (TODO figure out how to color this the same)
+- Consecutive `[` and `]` both to backticks.
+- \_arbitrary text\_ to \*arbitrary text\* if \_ preceded or followed by an alphanumeric or underscore.
+- If markdown lists with '*' don't work: Coqdoc lists (with '-') to markdown lists (with '*')
+
+---
+
+Old stuff:
+
+### Unintentional comment start/end
+
+Coq uses `(*` and `*)` to denote comment start and end. These can be used recursively. If they are in text and are exported inside a `(** *)`, it will interfere with the formatting.
+Unfortunately, it is easy to unintentionally write these. For example, the following waterproof text sentence:
+
+> (Water *proof*) text
+
+is syntactically `(Water *proof*) text`, which inadvertently contains a comment ending in Coq. Therefore, we will add a special character to remove any comment start or end non-code. The above sentence will become `(Water *proof*💧) text`.
+
+TODO: maybe need to start enforcing matching of comments in Waterproof
+
+### String literals
+
+In CoQ, if a string literal is opened in a comment, everything that follows after it until the string literal is closed is considered part of the string and has no further syntactic interpretation.
+
+Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). To avoid an odd number of double quotes, we add an `"` to the end of the open comment in `text` if it contains an odd number of quotes.
+
+### Using \#{1-6}
+TODO: in principle we can ignore(?) this and tackle it in the Vue representation of blocks.
+In waterproof (markdown) we may start text with `# `, `## `, ..., `###### ` to indicate various levels of headings, but in coqdoc we must use `* `, `** `, `**** `. Hence, we translate `#{1-4} ` at the start of a block to `*{1-4} ` and back to `#{1-4}` again. **If there is `#{5,6}` I don't know what to do yet**.
+
+### Bold/italics
+In waterproof (markdown) we may use `**text**` and `*text*` to write bold/italics respectively. In coq, we can do emphasis (italics) with `_text_`. Bold is a bit harder, but we can use `#<strong>#text#</strong>#`.
+
+### Coqdoc escape characters
+To simply output the characters $, % and # and escaping their escaping role in coqdoc, these characters are be doubled. In coqdoc, `$text$` would output text in latex math-mode. **However, this does not work for HTML-output, so it is quite useless.** 
+It is a little bit of a problem, because stuff in # is simply discarded in latex output actually.
+https://coq.inria.fr/refman/using/tools/coqdoc.html#escaping-to-latex-and-html
+
+### Notebook or exercise sheet?
+
+Always import as notebook. So previously exported exercise sheet can become notebook.
+
+***Should this be different? We could import exercise sheets as exercise sheets, but they are mutable as .v files anyways, and this will also complicate the UI***