IT/Description/theories.tex

2209 Questa teoria � usata nello sviluppo della teoria word e fornisce anche
2215 La teoria \theoryimp{words} introduce una selezione di costanti ed operazioni polimorfiche, i cui tipi possono essere istanziati a parole di qualsiasi dimensione. Per esempio, l'addizione word
2221 Tutti i teoremi circa operazioni word si applicano a word di qualsiasi lunghezza\footnote{Si noti
2222 che � impossibile introdurre word di lunghezza zero perch� tutti i tipi
2234 \holtxt{word\_len:\worda\rarr\num}.
2280 L'operazione \holtxt{word\_concat:\worda\rarr\wordb\rarr\wordc} concatena parole. Si noti che il tipo restituito non � vincolato. Questo significa che due parole di sedici bit possono essere concatenate per dare una parola di qualsiasi lunghezza -- che pu� essere pi� piccola o pi� grande del valore atteso di 32. La funzione correlata \holtxt{word\_join} restituisce una parola della lunghezza attesa, cio� di tipo fcp{\bool}{$\alpha+\beta$}; comunque, l'operazione di concatenazione � pi� utile perch� spesso vogliamo \fcp{\bool}{\ty{32}} e non il logicamente distinto \fcp{\bool}{\ty{16}+\ty{16}}.
2316 Le funzioni \holtxt{word\_lsb}, \holtxt{word\_msb} e \holtxt{word\_bit(i)}
2319 field, o sotto-parole: \holtxt{word\_bits} (\holtxt{--}),  \holtxt{word\_signed\_bits} (\holtxt{---}), \holtxt{word\_slice} (\holtxt{''}) e
2320 \holtxt{word\_extract} (\holtxt{><}). Per esempio, \holtxt{word\_bits 4 1} selezioner� quattro bit iniziando dalla posizione bit 1. La funzione slice � una variante in-place 8azzeira i bit fuori dal bit range) e la funzione extract combina \holtxt{word\_bits} con un cast di parola (\holtxt{w2w}). L'operazione \holtxt{word\_signed\_bits} � analoga a \holtxt{word\_bits}, eccetto che segna-estende il bit field.
2331 L'ordinamento di un bit di parola pu� essere capovolto con \holtxt{word\_reverse}, cio� il bit zero � scambiato con il bit $n - 1$ e cos� via.
2334 \holtxt{word\_modify:(\num\,\rarr\,\bool\,\rarr\,\bool)\,\rarr\,\worda\,\rarr\,\worda} cambia
2339 \holtxt{word\_modify ($\lambda$i b.\,if EVEN i then $\sim$b else b) w}
2351 (\holtxt{word\_rrx}). Questi shisft sono illustrati nella Figura~\ref{fig:shifts} e sono definiti in un maniera analoga alle operazioni bit field. Per
2376 word\_rrx (c,v)}.}
2404 La teoria word definisce anche alcune costanti parola:
2412 \holtxt{word\_T} or \holtxt{UINT\_MAXw} & $2^l - 1$ & $11\cdots 11$ \\
2413 \holtxt{word\_L} or \holtxt{INT\_MINw} & $2^{l - 1}$ & $10\cdots 00$ \\
2414 \holtxt{word\_H} or \holtxt{INT\_MAXw} & $2^{l - 1} - 1$ & $01\cdots 11$
2449 \holtxt{w2w} & & \worda\rarr\wordb & Map word-to-word (unsigned) \\
2450 \holtxt{sw2sw} & & \worda\rarr\wordb & Map word-to-word (signed) \\
2451 \holtxt{w2l} & & \num\rarr\worda\rarr\num~\ty{list} & Map word to digit list \\
2452 \holtxt{l2w} & & \num\rarr\num~\ty{list}\rarr\worda & Map digit list to word \\
2453 \holtxt{w2s} & & \num\rarr(\num\rarr\ty{char})\rarr\worda\rarr\ty{string} & Map word to string \\
2454 \holtxt{s2w} & & \num\rarr(\ty{char}\rarr\num)\rarr\ty{string}\rarr\worda & Map string to word \\
2455 \holtxt{word\_len} & & \worda\rarr\num & The word length \\
2456 \holtxt{word\_lsb} & & \worda\rarr\bool & The least significant bit \\
2457 \holtxt{word\_msb} & & \worda\rarr\bool & The most significant bit \\
2458 \holtxt{word\_bit} & & \num\rarr\worda\rarr\bool & Test bit position \\
2459 \holtxt{word\_bits} & \holtxt{--} & \num\rarr\num\rarr\worda\rarr\worda & Select a bit field \\
2460 \holtxt{word\_signed\_bits} & \holtxt{---} & \num\rarr\num\rarr\worda\rarr\worda & Sign-extend selected bit field \\
2461 \holtxt{word\_slice} & \holtxt{''} & \num\rarr\num\rarr\worda\rarr\worda &  Set bits outside field to zero \\
2462 \holtxt{word\_extract} & \holtxt{><} & \num\rarr\num\rarr\worda\rarr\wordb & Extract (cast) a bit field \\
2463 \holtxt{word\_reverse} & & \worda\rarr\worda & Reverse the bit order \\
2465 \holtxt{word\_modify} & & {\setlength{\tabcolsep}{0pt}\begin{tabular}[t]{ll}(\num\rarr\bool\rarr\bool)\rarr\\\worda\rarr\worda\end{tabular}} & Apply a function to each bit \\
2466 \holtxt{word\_join} & & \worda\rarr\wordb\rarr\fcp{\bool}{$\alpha+\beta$} & Join words \\
2467 \holtxt{word\_concat} & \holtxt{@@} & \worda\rarr\wordb\rarr\wordc & Concatenate words \\
2469 \holtxt{word\_replicate} & & \num\rarr\worda\rarr\wordb & Replicate word \\
2470 \holtxt{word\_or} & \holtxt{||} & \worda\rarr\worda\rarr\worda & Bitwise disjunction \\
2471 \holtxt{word\_xor} & \holtxt{??} & \worda\rarr\worda\rarr\worda & Bitwise exclusive-or \\
2472 \holtxt{word\_and} & \holtxt{\&\&} & \worda\rarr\worda\rarr\worda & Bitwise conjunction \\
2473 \holtxt{word\_nor} & \holtxt{\~{}||} & \worda\rarr\worda\rarr\worda & Bitwise NOR \\
2474 \holtxt{word\_xnor} & \holtxt{\~{}??} & \worda\rarr\worda\rarr\worda & Bitwise XNOR \\
2475 \holtxt{word\_nand} & \holtxt{\~{}\&\&} & \worda\rarr\worda\rarr\worda & Bitwise NAND \\
2476 \holtxt{word\_reduce} & & {\setlength{\tabcolsep}{0pt}\begin{tabular}[t]{ll}(\bool\rarr\bool\rarr\bool)\rarr\\\worda\rarr\fcp{\bool}{1}\end{tabular}} & Word reduction \\
2483 \holtxt{word\_{}1comp} & \holtxt{\~} & \worda\rarr\worda & One's complement \\
2484 \holtxt{word\_{}2comp} & \holtxt{-} & \worda\rarr\worda & Two's complement \\
2485 \holtxt{word\_add} & \holtxt{+} & \worda\rarr\worda\rarr\worda & Addition \\
2486 \holtxt{word\_sub} & \holtxt{-} & \worda\rarr\worda\rarr\worda & Subtraction \\
2487 \holtxt{word\_mul} & \holtxt{*} & \worda\rarr\worda\rarr\worda & Multiplication \\
2488 \holtxt{word\_div} & \holtxt{//} & \worda\rarr\worda\rarr\worda & Division (unsigned) \\
2489 \holtxt{word\_sdiv} & \holtxt{/} & \worda\rarr\worda\rarr\worda & Division (signed) \\
2490 \holtxt{word\_mod} & & \worda\rarr\worda\rarr\worda & Modulus \\
2491 \holtxt{word\_log2} & & \worda\rarr\worda & Logarithm base-2 \\
2492 \holtxt{word\_lsl} & \holtxt{<<} & \worda\rarr\num\rarr\worda & Logical shift left \\
2493 \holtxt{word\_lsr} & \holtxt{>>>} & \worda\rarr\num\rarr\worda & Logical shift right \\
2494 \holtxt{word\_asr} & \holtxt{>>} & \worda\rarr\num\rarr\worda & Arithmetic shift right \\
2495 \holtxt{word\_ror} & \holtxt{\#>>} & \worda\rarr\num\rarr\worda & Rotate right \\
2496 \holtxt{word\_rol} & \holtxt{\#<<} & \worda\rarr\num\rarr\worda & Rotate left \\
2497 \holtxt{word\_rrx} & & \bool\#\worda\rarr\bool\#\worda & Rotate right extended by 1 place \\
2498 \holtxt{word\_lt} & \holtxt{<} & \worda\rarr\worda\rarr\bool & Signed ``less than'' \\
2499 \holtxt{word\_le} & \holtxt{<=} & \worda\rarr\worda\rarr\bool & Signed ``less than or equal'' \\
2500 \holtxt{word\_gt} & \holtxt{>} & \worda\rarr\worda\rarr\bool & Signed ``greater than'' \\
2501 \holtxt{word\_ge} & \holtxt{>=} & \worda\rarr\worda\rarr\bool & Signed ``greater than or equal'' \\
2502 \holtxt{word\_lo} & \holtxt{<+} & \worda\rarr\worda\rarr\bool & Unsigned ``less than''  \\
2503 \holtxt{word\_ls} & \holtxt{<=+} & \worda\rarr\worda\rarr\bool & Unsigned ``less than or equal'' \\
2504 \holtxt{word\_hi} & \holtxt{>+} & \worda\rarr\worda\rarr\bool & Unsigned ``greater than'' \\
2505 \holtxt{word\_hs} & \holtxt{>=+} & \worda\rarr\worda\rarr\bool & Unsigned ``greater than or equal'' \\