# Readme

Guide to Sail, as of August 6 2014. Subject to possible change later.

Sail relies on external access to Lem, Ott, Lem libraries, and Power
binaries for some testing, as well as Ocaml 4.01.0 or later. Some 
dependencies are at present hard coded paths in makefiles. Thus 
Sail expects to find a directory structure as the following
External directory structure:
Sail to be found in BASE/bitbucket/l2
Lem to be found in BASE/bitbucket/lem
idl to be found in BASE/rsem/idl

(BASE might have to be the user homedirectory, but many connections
are using ../../ etc)

Sail sources and binaries are to be found in the directories of
bitbucket/l2 (to be renamed when we make sail public in a
bitbucket/sail respository (hopefully)

Top level directories
src/            ML implementation of Sail frontend, Sail executable, subdirectories
language/       Ott definitions of source language, pdfs as well
l3-to-l2/       Directory for student to define l3-to-l2 translation, abandoned?

Relevant make commands:
make            Builds Sail executable
make test       As above, also builds interpreter, and runs test suite
make power      As above (except running) and  builds executable interpreting power binary
make clean      Cleans src and language


language directory
l2_parse.ott    Grammar of Sail generated by parser, superset of source language
l2.ott          Grammar of Sail source
l2_typ.ott      Grammar of Internal structures used for type annotations
l2_rules.ott    Rules for type system

Relevant make commands:
make          Builds pdfs for l2 and l2_parse, ml and lem files of grammars

Generated files
l2.pdf          combines grammar of l2.ott l2_typ.ott and rules of l2_rules.ott
l2_parse.pdf    grammar of l2_parse.ott only
l2.ml           grammar of l2.ott only, used by type checker
l2_parse.ml     grammar of l2_parse.ott only, used by parser and initial check
l2.lem          combines grammar of l2.ott and l2_typ.ott, used by interpreter

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
initial_check.ml        translate l2_parse grammar to l2 grammar
lem_interp/             source directory of interpreter
lexer.mll               
myocamlbuild.ml
parse_ast.ml            symlink to language/l2_parse.ml
parse.mly
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
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
sail.ml                 main file
sail.native             executable for Sail
sail_lib.ml             treat some sail functions as a library, for idl/power generation
test/                   directory of test suite
type_check.ml           Main type checker
type_internal           Structure of internal types, and type - type comparisons
util.ml

Relevant make commands:
make            Builds Sail executable (does not remake language files automatically)
make test       As above, also builds interpreter, and runs test suite
make power      As above (except running) and  builds executable interpreting power binary
make test_power As above, runs power binary found in idl/power/binary
make clean      

Using sail executable
./sail.native -h   % Lists command line flags
./sail.native test.sail -lem_ast % typical usage to generate a lem_ast file test.lem
./sail.native test.sail -verbose % resulting sail is not typecheckable

lem_interp directory
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
pretty_interp.ml        pretty printing for interperter forms
run_interp.ml           interactive implementation for running interpreter with simple memory and registers


test directory
idempotence.sh          script to test the pretty printer, but files might not pass type checking for predictable reasons
pattern.sail            part of test suite, testing pattern match
power.sail              extract of subset of power instructions: NOT JUST USED FOR TESTING
regbits.sail            part of test suite, testing register declarations
run_power.ml            framework to read memory, and run power in interpreter
run_tests.ml            framework for running test suite
testN.sail              various test suite files, based on past bugs
vectors.sail            part of test suite, testing vector operations