IT/Description/definitions.tex

18 ricorsive, ricorsive annidate, e coinvolgere record. La sintassi delle
30 \newcommand{\recdspec}  {\mbox{\it record-spec}}
249 Tipi record semplici possono essere introdotti usando la notazione \holtxt{<| ... |>}.
258 L'uso di tipi record pu� essere ricorsivo. Per esempio, la seguente
393 Quando � definito un tipo che coinvolge record, molte pi� definizioni sono
400 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!tipi record}
401 \index{tipi record}
403 I tipi record sono dei modi convenienti d'impacchettare insieme un numero di
405 l'accesso ad essi. I tipi record sono semanticamente equivalenti a grandi
407 propria scelta � una grande comodit�. I tipi record come
409 record del Pascal.
411 Costruiti correttamente, i tipi record forniscono utili funzionalit� di manutenibilit�.
412 Se si pu� sempre accedere al campo {\tt fieldn} di un tipo record
413 semplicemente scrivendo {\tt record.fieldn}, allora dei cambiamenti al tipo che
415 questo riferimento. Una mancanza nei tipi record dell'SML � che non
417 (funzionali) dei record. L'implementazione HOL permette di scrivere
423 che sostituisce il vecchio valore di {\tt fieldn} nel record {\tt rec}
426 del record.
428 \paragraph{Definire un tipo record}
429 I tipi record sono definiti con la funzione \texttt{Hol\_datatype}, come
430 discusso in precedenza. Per esempio, per creare un tipo record chiamato
446    $\langle$\textsl{record-type\/}$\rangle$\verb|_|$\langle$\textsl{field\/}$\rangle$.
448 di accesso ai campi per accedere ai valori del campo di un record. Cos�,
452 stampata usando la prima sintassi, con il punto.\index{tipi record!notazione di selezione dei campi}
455 \mbox{``$\langle$\textsl{record-type}$\rangle$\texttt{\_}$\langle$\textsl{field}$\rangle$\texttt{\_fupd}''}
457 tipo. Esse prendono due argomenti, una funzione e un record da
459 cos� che il record risultante � lo stesso dell'originale, eccetto per il fatto che
471 � un valore record identico a \texttt{bob} eccetto per il fatto che il
475 record con uno dei suoi campi sostituito da un valore specifico. Questo �
516 \paragraph{Specificare letterali record}
530 \paragraph{Usare i teoremi prodotti da definizioni di record}
533 di tipo record dimostra anche una suite di utili teoremi. Questi sono tutti
577 pacchetto tipi record cresce come il quadrato del numero di campi nel
578 record. (In particolare, i teoremi di canonicalizzazione dell'aggiornamento e
580 con record grandi, l'implementazione dei tipi record usa una
587 Sfortunatamente, la rappresentazione di record grandi ha lo svantaggio che
591 ammette l'uso di teoremi pi� piccoli quando dei valori record sono
593 dall'utente che menzionano campi di record grandi o aggiornamenti di campi passino
597 Il pretty-printing di record grandi pu� essere controllato con il
656 record con i seguenti campi.
658 {\it types\/} � una lista di record, ognuno dei quali contiene due campi:
684 {\it defs\/} � una lista di record che specifica le costanti da sollevare.
685 Ciascun record contiene i seguenti quattro campi:
747 record con gli stessi campi di sopra eccetto per {\it old\_thms},