Support for literate SAW files

[weaversa]

Here is an ask for saw to accept and parse (as an argument to include or via command-line input) literate files. I imagine markdown, or whatever subset of formats Cryptol currently accepts would be appropriate. I have an example file test.md below. Currently saw is unable to accept this file as input. Note that saw does currently accept literate Cryptol files, just not literate SAW files, so the import "test.md" as test command currently succeeds when run in the saw interpreter.

---

Introduction

This is a test of combining Cryptol and SAW in the same Markdown document

Cryptol

module test where

x = 1

SAW

import "test.md" as test

let y = 10;

print {{ test::x + y }};

[msaaltink]

Let me second this great idea. It could really make the presentation of a SAW file look a lot nicer. Combining a Cryptol file with the SAW that contains its proofs is also very neat.

[robdockins]

Another possibility to consider is to use one of the several existing language-agnostic literate programming preprocessors. I know of noweb and nuweb (both successors of WEB). Both have the ability to help typeset documents, and produce multiple related source files in potentially different languages for further processing.

[weaversa]

I've recently seen a really nice demo of using Cryptol + SAW + C w/ nuweb and it is quite expressive, powerful, and easy to use if you already know LaTeX. I'll see if I can share it. I also think the lighter-weight markdown in SAW would still be useful.

[robdockins]

I think it would be pretty easy to add a "basic" literate mode where code blocks are interpreted as SAW, and code blocks with the "cryptol" tag are implemented the same way as inline let {{ }} blocks.

Implementing full Cryptol modules would probably be considerably more difficult, and should maybe be the realm of these external tools we mentioned above.

[weaversa]

@robdockins SAW current works just fine parsing out full-featured literate Cryptol. SAW is just missing the ability to parse "saw" tags in markdown files. The example in the first post uses both parsers (include and import) to consume the file twice, as it were.