diff options
Diffstat (limited to 'language/primitive_doc.ott')
| -rw-r--r-- | language/primitive_doc.ott | 118 |
1 files changed, 118 insertions, 0 deletions
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 + |