finish online docs?

docs/online.md

@@ -64,21 +64,52 @@ For instance, there are corresponding functions for expressions:
 val dis_expr : AST.l -> AST.expr -> sym rws
 val eval_expr : AST.l -> Env.t -> AST.expr -> value
 ```
-Here, the _'a rws_ return value is a computation inside the reader-writer-state monad:
-```
+Here, the _'a rws_ return value is a computation inside the reader-writer-state monad (discussed below).
+
+The entry-point to the entire partial evaluator is the _dis\_core_ method.
+This invokes the appropriate "dis" functions then performs a number of post-processing
+transformations, described next.
+
+#### LocalEnv / DisEnv
+
+The LocalEnv structure stores and manipulates location-sensitive information during the
+partial evaluation.
+Most importantly, this includes the stack 
+mappings of variables to their concrete value or pure symbolic expression.
+To facilitate easier debugging, this also manually records a stack of the
+AST nodes currently being evaluated
+(the ordinary stack trace is not useful in the presence of the monad abstraction).
+
+The DisEnv contains the _'a rws_ type — a reader-writer-state monad:
+```ocaml
 type 'a rws = Eval.Env.t -> LocalEnv.t -> ('a, LocalEnv.t, stmt list)
 ```
 This implements an abstraction for:
 - a read-only view of globals and constants ("eval env"),
-- a mutable state with a mapping of variables to their concrete value or pure symbolic expression ("local env"), and
+- a mutable LocalEnv state ("local env"), and
 - a write-only list of statements making up the residual program.
 
-This mechanism is invoked in the `let@` and `let+` syntaxes
-which composes RWS computations in a sensible way (explained more below, if desired).
-
-The entry-point to the entire partial evaluator is the _dis\_core_ method.
-This invokes the appropriate "dis" functions then performs a number of post-processing
-transformations, described next.
+This mechanism is invoked by the `let@` and `let+` syntaxes
+which composes RWS computations in a sensible way.
+As an example, with many type annotations, consider
+```ocaml
+val int_is_zero : int rws -> bool rws =
+  fun (x : int rws) ->
+    let@ y : int = x in
+    DisEnv.pure (y = 0)  
+```
+Essentially, the `let@` notation has the function of "unwrapping" a rws computation
+and placing it within another rws computation.
+`let+` can be used where the final result (at the bottom of the let expression)
+is a `DisEnv.pure` computation.
+By using `let+`, the `DisEnv.pure` can be omitted.
+Other functions exist to manipulate particular rws computations in particular ways
+(e.g. a list of rws can become a rws of list).
+
+The DisEnv struct also contains methods to retrieve variables
+(searching the local bindings and then the global bindings),
+all returning rws computations.
+To emit a statement into the residual program, it provides a `write` function.
 
 ### transforms.ml
 
@@ -88,28 +119,38 @@ Some of these are conventional compiler transformations
 (e.g. removing unused variables, common subexpression factoring, and copy-propagation).
 The majority, however, are designed to address deficiencies
 (verbosity or unsupported constructs) in the residual program.
-We discuss a few transformations which are of particular interest.
-
-## StatefulIntToBits / IntToBits
-
-This transformation converts expressions involving arbitrary-precision integers
-into expressions of fixed-length bitvectors
-by way of an interval analysis.
-
-The StatefulIntToBits modules implements this through an abstract interpretation
-with an abstract domain of $\text{Width}\times \text{IsSigned} \times \mathbb Z^2$
-
-
-
-
-
+We list a few transformations which are of particular interest.
+
+- StatefulIntToBits / IntToBits:
+  This transformation converts expressions involving arbitrary-precision integers
+  into expressions of fixed-length bitvectors
+  by way of an interval analysis.
+
+  The StatefulIntToBits modules implements this through abstract interpretation
+  with a domain of $\text{Width}\times \text{IsSigned} \times \mathbb Z^2$,
+  recording bit-width, signedness, and lower and upper bounds.
+
+- RedundantSlice: Eliminates slice operations which do not reduce the bit-width.
+  Crucially, this is also responsible for converting slices with non-static indices
+  into shift/truncate operations.
+- bits_coerce_narrow: Pushes slices into sub-expressions where possible.
+- CaseSimp: Removes unreachable assertions placed after exhaustive case checks.
+- RemoveRegisters: Replaces expressions of ASL's register type with ordinary bit-vectors.
+- CopyProp
+- CommonSubExprElim
+- RemoveUnused
 
 ## Grammar
 
-## Supporting
+The ASL grammar is defined in [asl.ott](/libASL/asl.ott).
+The ott program translates this into a Menhir grammar
+which then generates a parser and an associated Ocaml AST.
+The generated code modules include Asl_ast, Asl_parser, and Asl_parser_pp.
+
 
-- asl_ast (auto-generated)
-- monads
-- asl\_utils
-- utils
+For printing AST nodes and other structures, functions beginning with `pp_` are available
+in [asl_utils.ml](/libASL/asl_utils.ml) and [utils.ml](/libASL/utils.ml).
+These will produce an indented human-readable string.
+To emit AST nodes in the structured "aslt" format,
+use `Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt)` or similar.
 

docs/vectoriser.md

@@ -0,0 +1,3 @@
+# vectoriser
+
+todo