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
128
129
130
|
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 'a. option < 'a > : Typ -> Typ :: :: optCtors
| 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 To add to a function val specification indicating that n relies on call site expected value }}
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**64 |] :: :: uintsixtyfourDesc
functions :: '' ::=
{{ com Built-in functions: all have effect pure, all order polymorphic }}
| val forall Typ 'a . 'a -> unit : ignore :: :: ignore
| val forall Typ 'a . 'a -> option < 'a > : Some :: :: some
| val forall Typ 'a . unit -> option < 'a > : None :: :: none
| val ( [: 'n :] , [: 'm :] ) -> [| 'n + 'm |] : + :: :: 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
|
