diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 5 | ||||
| -rw-r--r-- | language/l2.ott | 8 | ||||
| -rw-r--r-- | language/manual.pdf | bin | 391550 -> 0 bytes | |||
| -rw-r--r-- | language/manual.tex | 95 |
4 files changed, 7 insertions, 101 deletions
diff --git a/language/Makefile b/language/Makefile index 0c7563ce..1420ab1f 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,6 +1,6 @@ #OTT=../../../rsem/ott/bin/ott # this is the binary that gets rebuilt by make in ott/src: -OTT=../../../rsem/ott/src/ott +OTT=../../../github/ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all @@ -37,5 +37,6 @@ l2.lem: l2.ott l2_typ.ott clean: rm -rf *~ -rm -rf *.uo *.ui *.sig *.sml .HOLMK - -rm -f *.tex *.aux *.log *.dvi *.ps *.pdf + -rm -f *.aux *.log *.dvi *.ps *.pdf rm -rf l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem + rm -rf l2.tex doc_in.tex
\ No newline at end of file diff --git a/language/l2.ott b/language/l2.ott index efed02bd..c3807f6a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -122,7 +122,7 @@ id :: '' ::= | atom :: M :: atom {{ ichlo (Id "atom") }} | vector :: M :: vector {{ ichlo (Id "vector") }} | list :: M :: list {{ ichlo (Id "list") }} - | set :: M :: set {{ ichlo (Id "set") }} +% | set :: M :: set {{ ichlo (Id "set") }} | reg :: M :: reg {{ ichlo (Id "reg") }} | to_num :: M :: tonum {{ com Built in function identifiers }} {{ ichlo (Id "to_num") }} | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} @@ -135,7 +135,7 @@ id :: '' ::= % targets use alphabetical infix operators. kid :: '' ::= - {{ com variables with kind, ticked to differntiate from program variables }} + {{ com variables with kind, ticked to differentiate from program variables }} {{ aux _ l }} | ' x :: :: var @@ -687,7 +687,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} - | id ( exp1 , .. , expn ) :: :: memory {{ com memory write via function call }} + | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} | ( typ ) id :: :: cast | ( lexp0 , .. , lexpn ) :: :: tup {{ com set multiple at a time, a check will ensure it's not memory }} @@ -708,7 +708,7 @@ fexps :: 'FES_' ::= | fexp1 ; ... ; fexpn semi_opt :: :: Fexps opt_default :: 'Def_val_' ::= - {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ com Optional default value for indexed vectors, to define a default value for any unspecified positions in a sparse map }} {{ aux _ annot }} {{ auxparam 'a }} | :: :: empty | ; default = exp :: :: dec diff --git a/language/manual.pdf b/language/manual.pdf Binary files differdeleted file mode 100644 index d848b8da..00000000 --- a/language/manual.pdf +++ /dev/null diff --git a/language/manual.tex b/language/manual.tex index 86aaa8b0..5d4b9d6a 100644 --- a/language/manual.tex +++ b/language/manual.tex @@ -17,101 +17,6 @@ \newpage -\section{Introduction} - -This is a manual describing the Sail specification language, its -common library, compiler, interpreter and type system. However it is -currently in early stages of being written, so questions to the -developers are highly encouraged. - -\section{Tips for Writing Sail specifications} - -This section attempts to offer advice for writing Sail specifications -that will work well with the Sail executable interpreter and -compilers. - -These tips use ideomatic Sail code; the Sail syntax is formally -defined in following section. - -Some tips might also be advice for good ways to specify instructions; -this will come from a combination of users and Sail developers. - -\begin{itemize} - -\item Declare memory access functions as one read, one write announce, - and one write value for each kind of access. - -For basic user-mode instructions, there should be the need for only -one memory read and two memory write function. These should each be -declared using {\tt val extern} and should have effect {\tt wmem} and -{\tt rmem} accordingly. - -Commonly, a memory read function will take as parameters a size (an -number below 32) and an address and return a bit vector with length (8 -* size). The sequential and concurrent interpreters both only read and -write memory as a factor of bytes. - -\item Declare a default vector order - -Vectors can be either decreasing or increasing, i.e. if we have a -vector \emph{a} with elements [1,2,3] then in an increasing specification the 1 is accessed -with {\tt a[0]} but with {\tt a[2]} in a decreasing system. Early in -your specification, it is beneficial to clarity to say default Ord inc -or default Ord dec. - -\item Vectors don't necessarily begin indexing at 0 or n-1 - -Without any additional specification, a vector will begin indexing at -0 in an increasing spec and n-1 in a decreasing specification. A type -declaration can reset this first position to any number. - -Importantly, taking a slice of a vector does not reset the indexes. So -if {\tt a = [1,2,3,4]} in an increasing system the slice {\tt a[2 - ..3]} generates the vector {\tt [3,4]} and the 3 is indexed at 2 in either vector. - -\item Be precise in numeric types. - -While Sail includes very wide types like int and nat, consider that -for bounds checking, numeric operations, and and clear understanding, -these really are unbounded quantities. If you know that a number in -the specification will range only between 0 and 32, 0 and 4, $-32$ to -32, it is better to use a specific range type such as $[|32|]$. - -Similarly, if you don't know the range precisely, it may also be best -to remain polymorphic and let Sail's type resolution work out bounds -in a particular use rather than removing all bounds; to do this, use -[:'n:] to say that it will polymorphically take some number. - -\item Use bit vectors for registers. - -Sail the language will readily allow a register to store a value of -any type. However, the Sail executable interpreter expects that it is -simulating a uni-processor machine where all registers are bit -vectors. - -A vector of length one, such as \emph{a} can read the element of \emph{a} -either with {\tt a} or {\tt a[0]}. - -\item Have functions named decode and execute to evaluate - instructions. - -The sail interpreter is hard-wired to look for functions with these names. - -\item Type annotations are necessary to read the contents of a - register into a local variable. - -The code {\tt x := GPR[4]}, where GPR is a vector of general purpose -registers, will store a local reference to the fourth general purpose -register, not the contents of that registe, i.e. this will not read -the register. To read the register contents into a local variable, the -type is required explicitly so {\tt (bit[64]) x := GPR[4]} reads the -register contents into x. The type annotation may be on either side of -the assignment. - -\end{itemize} - - - \section{Sail syntax} \ottgrammartabular{ |