1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
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
|
