104 translations |
104 translations |
105 "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>" |
105 "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>" |
106 "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>" |
106 "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>" |
107 |
107 |
108 -- "function codes for unary operations" |
108 -- "function codes for unary operations" |
109 datatype unop = UPlus -- {*{\tt +} unary plus*} |
109 datatype unop = UPlus |
110 | UMinus -- {*{\tt -} unary minus*} |
110 | UMinus |
111 | UBitNot -- {*{\tt ~} bitwise NOT*} |
111 | UBitNot |
112 | UNot -- {*{\tt !} logical complement*} |
112 | UNot |
113 |
113 |
114 -- "function codes for binary operations" |
114 -- "function codes for binary operations" |
115 datatype binop = Mul -- {*{\tt * } multiplication*} |
115 datatype binop = Mul |
116 | Div -- {*{\tt /} division*} |
116 | Div |
117 | Mod -- {*{\tt %} remainder*} |
117 | Mod |
118 | Plus -- {*{\tt +} addition*} |
118 | Plus |
119 | Minus -- {*{\tt -} subtraction*} |
119 | Minus |
120 | LShift -- {*{\tt <<} left shift*} |
120 | LShift |
121 | RShift -- {*{\tt >>} signed right shift*} |
121 | RShift |
122 | RShiftU -- {*{\tt >>>} unsigned right shift*} |
122 | RShiftU |
123 | Less -- {*{\tt <} less than*} |
123 | Less |
124 | Le -- {*{\tt <=} less than or equal*} |
124 | Le |
125 | Greater -- {*{\tt >} greater than*} |
125 | Greater |
126 | Ge -- {*{\tt >=} greater than or equal*} |
126 | Ge |
127 | Eq -- {*{\tt ==} equal*} |
127 | Eq |
128 | Neq -- {*{\tt !=} not equal*} |
128 | Neq |
129 | BitAnd -- {*{\tt &} bitwise AND*} |
129 | BitAnd |
130 | And -- {*{\tt &} boolean AND*} |
130 | And |
131 | BitXor -- {*{\tt ^} bitwise Xor*} |
131 | BitXor |
132 | Xor -- {*{\tt ^} boolean Xor*} |
132 | Xor |
133 | BitOr -- {*{\tt |} bitwise Or*} |
133 | BitOr |
134 | Or -- {*{\tt |} boolean Or*} |
134 | Or |
135 text{* The boolean operators {\tt &} and {\tt |} strictly evaluate both |
135 |
136 of their arguments. The lazy operators {\tt &&} and {\tt ||} are modeled |
|
137 as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and |
|
138 {\tt a || b = a?true:b} |
|
139 *} |
|
140 datatype var |
136 datatype var |
141 = LVar lname(* local variable (incl. parameters) *) |
137 = LVar lname(* local variable (incl. parameters) *) |
142 | FVar qtname qtname bool expr vname |
138 | FVar qtname qtname bool expr vname |
143 (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90) |
139 (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90) |
144 | AVar expr expr (* array component *) ("_.[_]"[90,10 ]90) |
140 | AVar expr expr (* array component *) ("_.[_]"[90,10 ]90) |