DLTree (nholz)

DLTree Module

Namespace: HOL
Assembly: nholz.dll

Questo modulo costituisce una libreria di operazioni su alberi dinamici di ricerca - alberi binari auto-bilanciati che memorizzano informazioni su nodi ordinati in base a un indice rispetto alla relazione (<).

Types

Type	Description
dltree<'a, 'b>	Il datatype 'dltree' è un datatype di albero di ricerca binario, dove ad ogni nodo sono mantenuti un indice e un elemento, e le foglie non hanno alcuna informazione. Il confronto tra indici è fatto usando la relazione di oridinamento totale polimorfica '(<)'. Ogni nodo mantiene anche un intero per il suo livello AA, per poter mantenere l'invariante AA. Si noti che non c'è alcuna necessità che le foglie mantengano il proprio livello perché esso è sempre 0.

Type

Description

dltree<'a, 'b>

Il datatype 'dltree' è un datatype di albero di ricerca binario, dove ad ogni nodo sono mantenuti un indice e un elemento, e le foglie non hanno alcuna informazione. Il confronto tra indici è fatto usando la relazione di oridinamento totale polimorfica '(<)'. Ogni nodo mantiene anche un intero per il suo livello AA, per poter mantenere l'invariante AA. Si noti che non c'è alcuna necessità che le foglie mantengano il proprio livello perché esso è sempre 0.

Functions and values

Function or value	Description
`decrease_level l' tr` Full Usage: `decrease_level l' tr` Parameters: l' : `int` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`	Decresce il livello della radice di un albero a un dato livello più basso. Se il livello dato è maggiore o uguale al livello originario l'albero rimane invariato. l' : `int` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`
`dltree_delete x0 tr` Full Usage: `dltree_delete x0 tr` Parameters: x0 : `'a` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`	Cancella l'entry all'indice fornito in un dato albero di ricerca. Fallisce se l'albero non contiene alcuna entry per l'indice fornito. x0 : `'a` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`
`dltree_elem x0 tr` Full Usage: `dltree_elem x0 tr` Parameters: x0 : `'a` tr : `dltree<'a, 'b>` Returns: `'a * 'b`	Restituisce l'indice e l'elemento mantenuto all'indice fornito in un dato albero di ricerca. Fallisce se l'albero non ha entry per l'indice fornito. x0 : `'a` tr : `dltree<'a, 'b>` Returns: `'a * 'b`
`dltree_elems tr` Full Usage: `dltree_elems tr` Parameters: tr : `dltree<'a, 'b>` Returns: `('a * 'b) list`	Converte l'informazione mantenuta in un dato albero di ricerca binario in una lista di associazione ordinata per indice. tr : `dltree<'a, 'b>` Returns: `('a * 'b) list`
`dltree_empty` Full Usage: `dltree_empty` Returns: `dltree<'a, 'b>`	Restituisce un nuovo dltree vuoto. Returns: `dltree<'a, 'b>`
`dltree_insert (arg1, arg2) tr` Full Usage: `dltree_insert (arg1, arg2) tr` Parameters: arg0 : `'a` arg1 : `'b` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`	Inserisce in un dato albero di ricerca un singolo elemento indicizzato. Fallisce se l'albero contiene già un entry per l'indicie fornito. arg0 : `'a` arg1 : `'b` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`
`dltree_lookup x0 tr` Full Usage: `dltree_lookup x0 tr` Parameters: x0 : `'a` tr : `dltree<'a, 'b>` Returns: `'b`	Restituisce l'elemento mantenuto all'indice fornito in un dato albero di ricerca. x0 : `'a` tr : `dltree<'a, 'b>` Returns: `'b`
`dltree_mem x0 tr` Full Usage: `dltree_mem x0 tr` Parameters: x0 : `'a` tr : `dltree<'a, 'b>` Returns: `bool`	Restituisce "true" sse l'indice fornito occorre in un dato albero di ricerca. x0 : `'a` tr : `dltree<'a, 'b>` Returns: `bool`
`level tr` Full Usage: `level tr` Parameters: tr : `dltree<'a, 'b>` Returns: `int`	Restituisce il livello dell'albero. tr : `dltree<'a, 'b>` Returns: `int`
`right_app f tr` Full Usage: `right_app f tr` Parameters: f : `dltree<'a, 'b> -> dltree<'a, 'b>` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`	Applica una funzione al primo nodo più a destra di un albero. f : `dltree<'a, 'b> -> dltree<'a, 'b>` tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`
`rightmost_elem (arg1, arg2) tr` Full Usage: `rightmost_elem (arg1, arg2) tr` Parameters: arg0 : `'a` arg1 : `'b` tr : `dltree<'a, 'b>` Returns: `'a * 'b`	Restituisce come una coppia il nodo più a destra nell'albero. Se l'albero è solo una Leaf, allora non ha nodi e in questo caso la funzione restituisce solo la coppia in input. arg0 : `'a` arg1 : `'b` tr : `dltree<'a, 'b>` Returns: `'a * 'b`
`skew tr` Full Usage: `skew tr` Parameters: tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`	L'operazione skew esegue una singola rotazione a destra per ribilanciare quando il figlio sinistro ha lo stesso livello del suo padre. tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`
`split tr` Full Usage: `split tr` Parameters: tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`	L'operazione di split esegue una singola rotazione a sinistra per ribilanciare quando il nipote destro-destro ha lo stesso livello del suo nonno, incrementando il livello del nodo radice risultante. tr : `dltree<'a, 'b>` Returns: `dltree<'a, 'b>`