diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 7 | ||||
| -rw-r--r-- | language/l2.ott | 1 | ||||
| -rw-r--r-- | language/manual.tex | 84 | ||||
| -rw-r--r-- | language/primitive_doc.ott | 118 |
4 files changed, 209 insertions, 1 deletions
diff --git a/language/Makefile b/language/Makefile index 2076069c..594432fd 100644 --- a/language/Makefile +++ b/language/Makefile @@ -9,9 +9,16 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem %Theory.uo: %Script.sml Holmake --qof -I $(OTTLIB) $@ +manual.pdf: doc_in.tex manual.tex + pdflatex manual.tex + pdflatex manual.tex + l2.tex: l2.ott l2_typ.ott l2_rules.ott ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ +doc_in.tex: l2.ott primitive_doc.ott l2_typ.ott l2_rules.ott + ott -sort false -generate_aux_rules false -tex_wrap false -o $@ -picky_multiple_parses true $^ + %.tex: %.ott ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ diff --git a/language/l2.ott b/language/l2.ott index d65f1cb0..aa55b4eb 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -878,7 +878,6 @@ defs :: '' ::= - terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} diff --git a/language/manual.tex b/language/manual.tex new file mode 100644 index 00000000..d96e7263 --- /dev/null +++ b/language/manual.tex @@ -0,0 +1,84 @@ +\documentclass[11pt]{article} + +\usepackage{amsmath,amssymb,supertabular,geometry,fullpage} +\geometry{a4paper,twoside,landscape,left=10.5mm,right=10.5mm,top=20mm,bottom=30mm} +\usepackage{color} + +\begin{document} + +\input{doc_in} + +\title{Sail Manual} +\author{Kathryn E Gray, Gabriel Kerneis, Peter Sewell} + +\maketitle + +\tableofcontents + +\newpage + +\section{Sail syntax} + +\ottgrammartabular{ +\ottl\ottinterrule +\ottannot\ottinterrule +\ottid\ottinterrule +\ottkid\ottinterrule +\ottbaseXXkind\ottinterrule +\ottkind\ottinterrule +\ottnexp\ottinterrule +\ottorder\ottinterrule +\ottbaseXXeffect\ottinterrule +\otteffect\ottinterrule +\otttyp\ottinterrule +\otttypXXarg\ottinterrule +\ottnXXconstraint\ottinterrule +\ottkindedXXid\ottinterrule +\ottquantXXitem\ottinterrule +\otttypquant\ottinterrule +\otttypschm\ottinterrule +\ottnameXXscmXXopt\ottinterrule +\otttypeXXdef\ottinterrule +\otttypeXXunion\ottinterrule +\ottindexXXrange\ottinterrule +\ottlit\ottinterrule +\ottsemiXXopt\ottinterrule +\ottpat\ottinterrule +\ottfpat\ottinterrule +\ottexp\ottinterrule +\ottlexp\ottinterrule +\ottfexp\ottinterrule +\ottfexps\ottinterrule +\ottoptXXdefault\ottinterrule +\ottpexp\ottinterrule +\otttannotXXopt\ottinterrule +\ottrecXXopt\ottinterrule +\otteffectXXopt\ottinterrule +\ottfuncl\ottinterrule +\ottfundef\ottinterrule +\ottletbind\ottinterrule +\ottvalXXspec\ottinterrule +\ottdefaultXXspec\ottinterrule +\ottscatteredXXdef\ottinterrule +\ottregXXid\ottinterrule +\ottaliasXXspec\ottinterrule +\ottdecXXspec\ottinterrule +\ottdef\ottinterrule +\ottdefs\ottinterrule} + +\newpage +\section{Sail primitive types and functions} + +\ottgrammartabular{ +\ottbuiltXXinXXtypes\ottinterrule} + +\ottgrammartabular{ +\ottbuiltXXinXXtypeXXabbreviations\ottinterrule +\ottfunctions\ottinterrule +\ottfunctionsXXwithXXcoercions\ottinterrule} + +\section{Sail type system} + +\section{Sail operational semantics \{TODO\}} + +\end{document}
\ No newline at end of file diff --git a/language/primitive_doc.ott b/language/primitive_doc.ott new file mode 100644 index 00000000..2a0c2c0f --- /dev/null +++ b/language/primitive_doc.ott @@ -0,0 +1,118 @@ +grammar + +built_in_types :: '' ::= + {{ com Type Kind }} + | bit : Typ :: :: bitDesc + | unit : Typ :: :: unitDesc + | forall Nat 'n. Nat 'm. range <'n, 'm> : Nat -> Nat -> Typ :: :: rangeDesc + | forall Nat 'n, Nat 'm, Order 'o, Typ 't. vector < 'n, 'm, 'o, 't > : Nat -> Nat -> Order -> Typ :: :: vectorDesc + | forall Typ 't. register < 't > : Typ -> Typ :: :: registerDec + | forall Typ 't. reg < 't > : Typ -> Typ :: :: regDec + {{ com internal reference cell }} + | forall Nat 'n. implicit<'n> : Nat -> Typ :: :: implicitDesc + {{ com see Kathy for explanation }} + +built_in_type_abbreviations :: '' ::= + | bool => bit :: :: boolDesc + | nat => [| 0 '..' pos_infinity |] :: :: natDesc + | int => [| neg_infinity '..' pos_infinity |] :: :: intDesc + | uint8 => [| 0 '..' 2**8 |] :: :: uinteightDesc + | uint16 => [| 0 '..' 2**16 |] :: :: uintsixteenDesc + | uint32 => [| 0 '..' 2**32 |] :: :: uintthirtytwoDesc + | uint64 => [| 0 '..' 2**32 |] :: :: uintsixtyfourDesc + + +functions :: '' ::= + {{ com Built-in functions: all have effect pure, all order polymorphic }} + | val forall Typ 'a . 'a -> unit : ignore :: :: ignore + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'n + 'o '..' 'm + 'p |] : + :: :: plusbase + {{ com arithmetic addition }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : + :: :: plusvec + {{ com unsigned vector addition }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ]) -> ( bit [ 'n ] , bit , bit ) : + :: :: plusoverflow + {{ com unsigned vector addition with overflow, carry out }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : +_s :: :: plusvecS + {{ com signed vector addition }} + | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ] ) -> ( bit [ 'n ] , bit , bit ) : +_s :: :: plusoverflowS + {{ com signed vector addition with overflow, carry out }} + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'n - 'o '..' 'm - 'p |] : - :: :: minusbase + {{ com arithmetic subtraction }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : - :: :: minusvec + {{ com unsigned vector subtraction }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> ( bit [ 'n ] , bit , bit ) : - :: :: minusoverflow + {{ com unsigned vector subtraction with overflow, carry out }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : -_s :: :: minusvecS + {{ com signed vector subtraction }} + | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ] ) -> ( bit [ 'n ] , bit , bit ) : -_s :: :: minusoverflowS + {{ com signed vector subtraction with overflow, carry out }} + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'n * 'o '..' 'm * 'p |] : * :: :: multbase + {{ com arithmetic multiplication }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 2*'n ] : * :: :: multvec + {{ com unsigned vector multiplication }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 2*'n ] : *_s :: :: multvecS + {{ com signed vector multiplication }} + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 0 '..' 'p - 1 |] : mod :: :: modbase + {{ com arithmetic modulo, 'o $>$ 0 }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : mod :: :: modvec + {{ com unsigned vector modulo }} + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'q '..' 'r |] : quot :: :: quotbase + {{ com arithmetic integer division, 'o $>$ 0 }} + | val forall Nat 'n , Nat 'm . ( bit [ 'n ] , bit [ 'm ] ) -> bit [ 'n ] : quot :: :: quotvec + {{ com unsigned vector division }} + | val forall Nat 'n , Nat 'm . ( bit [ 'n ] , bit [ 'm ] ) -> bit [ 'n ] : quot_s :: :: quotvecS + {{ com signed vector division }} + | val forall Typ 'a , Nat 'n . ( 'a [' n] -> [| 'n '..' 'n |] ) : length :: :: len + | val forall Typ 'a , Nat 'n , Nat 'm , 'n <= 'm . ( implicit < 'm > , 'a [ 'n ] ) -> 'a [ 'm ] : mask :: :: mask + {{ com reduce size of vector, dropping MSBits. Type system supplies implicit parameter, uses may require a cast }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit : == :: :: vecEQ + {{ com vector equality }} + | val forall Typ 'a , Typ 'b . ( 'a , 'b ) -> bit : == :: :: EQ + | val forall Typ 'a , Typ 'b . ( 'a , 'b ) -> bit : != :: :: NEQ + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : < :: :: ltbase + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : < :: :: ltvec + {{ com unsigned less than }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : <_s :: :: ltvecS + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : > :: :: gtbase + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : > :: :: gtvec + {{ com unsigned greater than }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : >_s :: :: gtvecS + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : <= :: :: lteqbase + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : <= :: :: lteqvec + {{ com unsigned less than or eq }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : <=_s :: :: lteqvecS + | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> bit : >= :: :: gteqbase + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : >= :: :: gteqvec + {{ com unsigned greater than or eq }} + | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit : >=_s :: :: gteqvecS + | val bit -> bit : ~ :: :: neg + {{ com bit negation }} + | val forall Nat 'n . bit [ 'n ] -> bit [ 'n ] : ~ :: :: negvec + {{ com bitwise negation }} + | val ( bit , bit ) -> bit : | :: :: or + {{ com bitwise or }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : | :: :: orvec + | val ( bit , bit ) -> bit : & :: :: and + {{ com bitwise and }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : & :: :: andvec + | val ( bit , bit ) -> bit : ^ :: :: xor + {{ com bitwise xor ^ will fix gen later }} + | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : '^' :: :: xorvec + + +functions_with_coercions :: '' ::= + | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ]) -> [| 2 ** 'n |] : + :: :: plusvecRange + | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> bit [ 'n ] : + :: :: plusvecrange + | val forall Nat 'n, Nat 'o, Nat 'p. ( [| 'o '..' 'p |] , bit ['n] ) -> bit [ 'n ] : + :: :: plusrangevec + | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> [| 'o '..' 'p + 2** 'n |] : + :: :: plusvecrangeRange + | val forall Nat 'n ( bit [ 'n ] , bit ) -> bit [ 'n ] : + :: :: plusvecbit + | val forall Nat 'n ( bit , bit [ 'n ] ) -> bit [ 'n ] : + :: :: plusbitvec + | val forall Nat 'n . (bit [ 'n ] , bit [ 'n ]) -> [| 2 ** 'n |] : +_s :: :: plusvecRangeS + | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> bit [ 'n ] : +_s :: :: plusvecrangeS + | val forall Nat 'n, Nat 'o, Nat 'p. ( [| 'o '..' 'p |] , bit ['n] ) -> bit [ 'n ] : +_s :: :: plusrangevecS + | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> [| 'o '..' 'p + 2** 'n |] : +_s :: :: plusvecrangeRangeS + | val forall Nat 'n ( bit [ 'n ] , bit ) -> bit [ 'n ] : +_s :: :: plusvecbitS + | val forall Nat 'n ( bit , bit [ 'n ] ) -> bit [ 'n ] : +_s :: :: plusbitvecS + | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> bit [ 'n ] : - :: :: minusvecrange + | val forall Nat 'n, Nat 'o, Nat 'p. ( [| 'o '..' 'p |] , bit ['n] ) -> bit [ 'n ] : - :: :: minusrangevec + | val forall Nat 'n, Nat 'o, Nat 'p. ( bit [ 'n ] , [| 'o '..' 'p |] ) -> [| 'o '..' 'p + 2** 'n |] : - :: :: minusvecrangeRange + |