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. atom <'n> : Nat -> Typ :: :: atomDesc {{ com singleton number, instead of range<'n,'n> }}
  | 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 |] , [| 1 '..' 'p |] ) -> [| 0 '..' 'p - 1 |] : mod :: :: modbase
  {{ com arithmetic modulo }}
  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : mod :: :: modvec
  {{ com unsigned vector modulo }}
  | val ( [| 'n '..' 'm |] , [| 1 '..' 'p |] ) -> [| 'q '..' 'r |] : quot :: :: quotbase
  {{ com arithmetic integer division }}
  | 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 :] ) : 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 }}
  | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : '^' :: :: xorvec
  | val forall Nat 'n . ( bit ,  [| 'n |] ) -> bit [ 'n ] : '^^' :: :: duplicate
  {{ com duplicate bit into a vector }}
  | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : << :: :: lshift
  {{ com left shift }}
  | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : >> :: :: rshift
  {{ com right shift }}
  | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : <<< :: :: rotate
  {{ com rotate }}


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