Update READMEs [ci skip]

README.org

@@ -1,3 +1,5 @@
+* JSExplain
+
 To install:
 #+BEGIN_SRC shell
 make init
@@ -21,10 +23,18 @@ https://jscert.github.io/jsexplain/branch/master/driver.html
 mljsref results are tested online and results published to:
 https://psvg.doc.ic.ac.uk/ci/jscert-testing/
 
-* JavaScript features used
-- Object.assign
-- No type casting
-- No prototypes
-- Arrays (for tuples)
-- Switch on strings
-- ...
+** Architecture
+
+   The source code for the interpreter is primarily written in a subset of
+   OCaml with supporting runtime libraries written in both OCaml and JS.
+
+   The source code is located in the jsref directory. It can either be built
+   using the standard OCaml compiler (to produce a result we term mljsref), or
+   using a custom OCaml-to-JS compiler which is located in the generator
+   directory (we term the resulting product jsjsref).
+
+   Details about the custom compilation are provided in the generator
+   directory.
+
+   To simplify presentation of the code, a monadic binder syntax extension is
+   used. This is also described in the generator directory.

generator/README.org

@@ -64,6 +64,17 @@ type 'a tree =
 
 #+END_src
 
+    * *Records* Records are translated to objects. Record copying
+      `with` syntax is supported with any number of field updates.
+
+** About the Subset of JavaScript Used
+- Object.assign (ES6)
+- No type casting
+- No prototypes
+- Arrays (for tuples)
+- Switch on strings
+- ...
+
 ** Notes
 
    Historical versions of the repository required the OCaml 4.02.1 compiler
@@ -73,3 +84,28 @@ type 'a tree =
    the OCaml distribution into this directory, some further configuration may
    be required... Team members may find the whole historic distribution
    archived in the private jscert_dev repository.
+
+** About the Monadic Rewriter PPX
+   This is a OCaml AST preprocessor that converts `let%x` syntax into the
+   monadic binder `if_x` with the continuation as the bound expression of the
+   let term.
+
+   For example:
+   - `let%some x = expr in cont` becomes `if_some expr (fun x -> cont)`
+   - `let%if_spec (s,x) = expr in cont` becomes `if_spec expr (fun s x -> cont)`
+
+   The full list of available moands is provided in `monad_mapping` of
+   monad_ppx.ml, but is reproduced below for convenience:
+   - run
+   - string
+   - object
+   - value
+   - prim
+   - number
+   - some
+   - bool
+   - void
+   - success
+   - not_throw
+   - ter
+   - break