updated readme

1 files changed, 14 insertions, 4 deletions

diff --git a/README b/README
index fbc0fc4b..8f649a81 100644
--- a/README
+++ b/README
@@ -202,7 +202,9 @@ src directory (including some generated files)
 ast.ml                  symlink to language/l2.ml
 demo.sh                 script for setting up a demo
 finite_map.ml           utility implementation
+gen_lib/                source directory of libaries used by generated back ends
 initial_check.ml        translate l2_parse grammar to l2 grammar
+initial_check_full.ml   performs sames checks as above as to kind well-formedness but over l2 grammar
 lem_interp/             source directory of interpreter
 lexer.mll               
 myocamlbuild.ml
@@ -212,14 +214,14 @@ pp.ml                   utility for printing
 pprint/                 library directory of someone else's pretty printing combinators
 pre_lexer.mll           First pass lexer, to identify type identifiers
 pre_parser.mly          First pass parser, to identify type identifiers for actual parsing
-pretty_print.ml         our printers; one to Sail source, one to Lem ast
+pretty_print.ml         our printers; one to Sail source, one to Lem ast, one to Lem, and one to Ocaml
 process_file.ml
 reporting_basic.ml
-run_power.native        executable for interpreting power model with simple memory
-run_tests.native        executable to run test suite
+rewriter.ml             performs sail-to-sail transformations for various back ends
 sail.ml                 main file
 sail.native             executable for Sail
 sail_lib.ml             treat some sail functions as a library, for idl/power generation
+spec_analysis.ml        analyses a fully type annotated ast, primarily used by rewriters
 test/                   directory of test suite
 type_check.ml           Main type checker
 type_internal           Structure of internal types, and type - type comparisons
@@ -232,11 +234,19 @@ make run_mips.native Builds an executable sequential interpreter for MIPS Elf bi
 make clean      
 
 lem_interp directory
+instruction_extractor.lem processes a specification and identifies the ast nodes of instructions with appropriate tags to convert data types into/out of sail value type
 interp.lem              interpreter implementation
 interp_ast.lem          symlink to language/l2.lem
 interp_inter_imp.lem    implementation of externally visible interface
 interp_interface.lem    externally visible interface for memory
 interp_lib.lem          implementation of sail library functions
+interp_utilities.lem    commonly useful functions for interpreter
+sail_impl_base.lem      externally visible interface above interp_interface
 pretty_interp.ml        pretty printing for interperter forms
-run_interp.ml           interactive implementation for running interpreter with simple memory and registers
+run_interp.ml           interactive implementation for running interpreter with simple memory and registers, bitrotted
+run_interp_model.ml     interactive implementation for running sequential binaries
+run_with_elf.ml         hook run_interp_model up with elf support, main file of sequential interpreter
+run_with_elf_cheri.ml   as above but specific to cheri
+run_with_elf_cheri128.ml
+type_check.lem          implementation to type check fully inferenced, annotated, ast nodes (not complete)