Chapter 7 Le interfacce utente

L'ultimo tema già in parte affrontato nell'ambito del progetto HELM è quello dello sviluppo di interfacce responsabili di fornire un accesso uniforme ai moduli software che operino sul formato XML (si faccia riferimento alla figura 1.1 a pagina 14). In conformità al terzo requisito di HELM (pagina 13), sono state fornite due differenti interfacce: la prima permette l'accesso alle funzionalità della libreria tramite un comune browser ed è costituita dai siti di presentazione; la seconda è un'applicazione Gtk che è stata estesa per trasformarla in un prototipo per il browsing e la (ri)annotazione dei file della libreria.

7.1 I siti di presentazione

Per massimizzare la facilità di accesso ai documenti della libreria, è necessario effettuare tutta l'elaborazione sul lato server, permettendo agli utenti di utilizzare comuni browser come client. Al fine di non violare l'analogo requisito di HELM volto a massimizzare la facilità di pubblicazione, si richiede che tali server siano distinti da quelli di distribuzione. Questo porta alla nascita dei siti di presentazione, server HTTP che vengono contattati dagli utenti per effettuare le elaborazioni, come il proof-checking o l'applicazione di trasformazioni XSLT, e che a loro volta contattano i server di distribuzione per ottenere i necessari documenti XML.

Il prototipo di sito di presentazione che abbiamo sviluppato si basa su Cocoon, un framework per l'editoria Web basata su XML. Cocoon, che è un software free sviluppato nell'ambito dell'Apache XML Project¹, è un servlet Java che viene invocato dall'HTTP server ogni qualvolta viene richiesto un documento XML. L'elaborazione dei documenti effettuata da Cocoon si basa sul modello a pipeline, in cui il documento, sotto forma di albero DOM, viene generato da un processo sorgente, viene trasformato da una catena di processori e infine viene consumato da un processo pozzo. Usualmente, ma non necessariamente, il processo sorgente è un parser XML che, dato un file XML, ne ritorna l'albero DOM; il processo pozzo, invece, è un formatter che trasforma l'albero DOM nella rappresentazione testuale che verrà restituita dal Web server e che, normalmente, è un documento XML. Fra i possibili processori, quelli più utilizzati sono i processori XSLT, anche se ne esistono numerosi altri che, in genere, riconoscono esclusivamente gli elementi appartenenti ad un determinato namespace e li espandono in opportuni frammenti di alberi DOM, lasciando inalterata la restante struttura del documento. Un processore di questo genere è quello XSP (eXtensible Server Pages), che permette di aggiungere all'interno del documento elementi contenenti codice Java che verranno sostituiti dall'output della loro esecuzione. Per motivi di efficienza, la rappresentazione dei documenti nella pipeline, oltre che come albero DOM, può anche essere uno stream di eventi SAX oppure una struttura proprietaria, chiamata DTM, che è la più efficiente.

Ovviamente, è necessario un meccanismo per permettere a Cocoon di determinare la forma della pipeline da applicare ad un documento, ovvero l'esatta sequenza di processori da assemblare. Nelle prime versioni di Cocoon, indicate come 1.x, tale sequenza è indicata direttamente all'interno dei singoli documenti XML, per mezzo di processing instruction XML. Il problema di questo approccio è la mancata separazione fra contenuto ed elaborazione, reminescenza della mancata separazione fra contenuto e presentazione in HTML, superata dagli standard XML e XSLT. Nelle prossime versioni di Cocoon, ancora in via di sviluppo e complessivamente indicate come Cocoon 2, questo meccanismo verrà abbandonato e sostituito dalla site map, ovvero un file di configurazione che descriverà la funzione che ad ogni file XML fornito dal server associa la catena di processori da applicare.

Venendo al progetto HELM, un sito di presentazione deve essenzialmente fornire all'utente la possibilità di indicare non solo l'URI del file XML a cui è interessato, ma anche l'URI dell'eventuale annotazione da utilizzare, il formato di output richiesto e la lista delle notazioni da applicare.

Poiché, come nel caso del file contenente i tipi sintetizzati, ogni file di annotazione si riferisce ad uno e un solo file XML, nel caso in cui si specifichi una annotazione non è più necessario fornire l'URI del file XML. Inoltre, per gli stessi motivi esposti a pagina 118 per il caso particolare della sintesi delle prove in linguaggio naturale, è conveniente estendere le funzionalità del getter con interfaccia HTTP in modo che esponga un metodo che, dato un URI, se questo si riferisce ad una annotazione, allora viene restituito il documento sintetizzato a partire dall'annotazione e dal file a cui questa si riferisce, mentre se si riferisce ad un documento CIC, questo diventa l'output dell'esecuzione.

Vista l'osservazione precedente e poiché ad ogni coppia notazione--formato corrispondono due stylesheet XSLT, uno per la trasformazione dal livello del sistema logico a quello content e un altro per quella dal livello content a quello presentation, è sufficiente permettere all'utente di specificare, possibilmente in modo user-friendly,

l'URI dell'annotazione o del file a livello del sistema logico;
una lista di URI di stylesheet che complessivamente descrivano la trasformazione dal livello del sistema logico a quello content;
una lista di URI di stylesheet che complessivamente descrivano la trasformazione dal livello content a quello presentation.

Per evitare all'utente di doversi memorizzare gli URI degli stylesheet, l'interfaccia più semplice consiste, una volta che sia stato indicato l'URI del documento (o quello di una sua annotazione), nel fornire la lista degli stylesheet applicabili e la possibilità di indicare, per ognuno, se lo si voglia utilizzare o meno. Il problema si riduce, quindi, a quello di conoscere quali siano gli URI degli stylesheet, ovvero delle notazioni, rilevanti per un determinato documento. Poiché tale informazione è un tipico esempio di metadato e la gestione dei metadati non è stata ancora sviluppata, la costruzione di un'interfaccia user-friendly è stata momentaneamente sospesa.

Una volta specificati gli URI da utilizzare, resta il problema della sintesi, a partire dagli stylesheet indicati, dei due stylesheet da utilizzare rispettivamente nella trasformazione dal livello del sistema logico a quello content e da questo a quello presentation. Infatti, le singole notazioni non possono essere applicate sequenzialmente, ma solo contemporaneamente in quanto ognuna si attende come input il formato legato al sistema formale e restituisce come output il formato del livello content, impedendo cosí una loro serializzazione. Anche se il problema della serializzazione può essere risolto modificando l'architettura degli stylesheet, l'applicazione a cascata delle notazioni non è preferibile in quanto risulterebbe estremamente più costosa di quella parallela, che raggiunge già tempi di elaborazione spesso inaccettabili. Per combinare le notazioni in un unico stylesheet, è sufficiente creare un nuovo foglio di stile XSLT che importi quelli specificati; tale operazione è facilmente implementabile ricorrendo ad un CGI o ad una pagina XSP.

Infine, è necessario associare al documento XML scelto dall'utente la pipeline costituita, oltre che dal processo sorgente, dai due stylesheet sintetizzati come descritto in precedenza e dal processo formatter corrispondente al formato di output indicato dall'utente, per esempio HTML o XML. La soluzione adottata, in attesa dell'uscita di Cocoon 2, consiste in una pagina XSP (un processo sorgente) che, dati i tre URI necessari, produca in output l'albero DOM, ottenuto effettuando il parsing del documento matematico, a cui vengono aggiunti tre processing instruction indicanti rispettivamente l'URI del primo e del secondo stylesheet da applicare per mezzo di un processore XSLT e il formatter scelto (processo pozzo).

7.1.1 Risultati ottenuti

Nonostante il prototipo fornito sia già perfettamente funzionante, restano due problemi che ne precludono seriamente l'utilizzo:

La mancanza di browser in grado di riconoscere il formato MathML
Gli elevati tempi di elaborazione

Il primo problema è solo temporaneo in quanto le principali case produttrici di browser stanno aggiungendo il supporto per MathML ai loro prodotti, anche se lo sviluppo procede molto lentamente a causa dello scarso interesse commerciale dovuto al basso numero di potenziali utilizzatori di MathML. Per ovviare parzialmente al problema, è stato realizzato dal Dott. Luca Padovani nell'ambito del progetto HELM un widget Gtk realizzato in C++, chiamato MathView, per la resa delle espressioni MathML presentation che compaiano all'interno di documenti XML. Il widget, del quale è stata rilasciata la prima versione stabile, riconosce tutti gli elementi e gli attributi di presentation markup descritti dalla specifica, a cui è pienamente conforme (ad eccezione dei due valori ``leftoverlap'' e ``rightoverlap'' dell'attributo ``side'' dell'elemento ``mtable'' che non vengono riconosciuti), ed è la prima implementazione che gestisce automaticamente il layout di formule di arbitraria grandezza; inoltre, ha un meccanismo che permette la selezione esclusivamente di alcune sottoformule, determinate dalla presenza di un attributo opzionale sul nodo radice.

Il secondo problema non è di facile soluzione ed è una diretta conseguenza delle scarse prestazioni degli attuali processori XSLT, tutti scritti in linguaggio Java. Nel giro di pochi mesi si attende l'uscita di una nuova generazione di processori, scritti in differenti linguaggi e con un particolare riguardo per le prestazioni, che dovrebbero alleviare il problema: il prototipo più avanzato di processore XSLT scritto in C++, Xalan-C², è circa un ordine di grandezza più veloce della corrispondente implementazione in Java. Tale incremento di prestazioni, comunque, nonostante renderebbe accettabili i tempi di elaborazione per i documenti più semplici, non sarebbe ancora sufficiente per quelli più complessi, che oggi richiedono tempi superiori ai dieci minuti.

7.2 L'interfaccia sviluppata in Gtk

La creazione di siti di presentazione permette di usufruire della libreria di HELM senza la necessità di installare sulla macchina dell'utente alcun tipo di software, ma non permette di contribuire alla libreria, per esempio annotandone alcuni degli oggetti o esportando nuove teorie: tali operazioni, per motivi essenzialmente prestazionali, debbono essere svolte sul lato client. Pertanto, è stata sviluppata un'interfaccia grafica in Gtk, l'emergente standard per la realizzazione di interfacce grafiche in ambiente Unix, scritta in OCaml. Successivamente, l'interfaccia è stata estesa, trasformandola in un prototipo di interfaccia per la (ri)annotazione delle prove; le funzionalità attualmente messe a disposizione sono:

Visualizzazione di un menu ad albero in cui sono riportati tutti gli oggetti e le teorie a conoscenza del getter.
Visualizzazione degli oggetti o delle teorie in formato MathML presentation, ottenuto applicando agli oggetti le trasformazioni descritte nel precedente capitolo³.
Possibilità di invocare il proof-checker sull'oggetto o la teoria attualmente visualizzati.
Navigazione ipertestuale ottenuta tramite hyperlink che associano alle occorrenze dei nomi degli oggetti le loro definizioni⁴.
Possibilità di selezionare esclusivamente le espressioni che corrispondono alla presentazione di un nodo CIC annotabile.
Possibilità di (ri)annotare il nodo selezionato scrivendo manualmente il markup che costituisce l'annotazione. Per l'introduzione degli elementi di ricorsione e di quelli che selezionano gli attributi del nodo corrente, l'interfaccia propone anche una palette dei suggerimenti: ogni pulsante della palette, quando premuto, inserisce nella posizione corrente dell'annotazione il markup corrispondente al suggerimento.

Nel prossimo paragrafo verranno descritte le principali scelte progettuali. La descrizione dell'implementazione viene, invece, omessa in quanto non ha presentato particolari difficoltà.

7.2.1 Progettazione

Lo sviluppo del prototipo è stato articolato in due fasi distinte: nella prima è stata sviluppata l'interfaccia Gtk nella quale sono stati integrati il proof-checker sviluppato nel capitolo 5, un processore XSLT e, come browser per MathML presentation, il widget MathView; nella seconda fase è stato aggiunto il supporto per la (ri)annotazione.

Prima fase

Le scelte progettuali preliminari alla progettazione della prima fase sono state:

L'interfaccia deve basarsi sull'emergente standard Gtk per sfruttarne le caratteristiche di portabilità. La libreria Gtk, infatti, è oggi disponibile per diverse architetture e sotto diversi sistemi operativi; inoltre, esistono binding per Gtk per tutti i linguaggi di programmazione più diffusi, compreso OCaml.
Deve essere possibile con poco sforzo implementativo utilizzare un qualunque processore XSLT scritto in un qualunque linguaggio. L'obiettivo è quello di massimizzare la modularità ed è reso particolarmente significativo dalle scarse prestazioni degli attuali processori: deve essere possibile utilizzare in ogni momento quello dalle prestazioni migliori.
Il linguaggio utilizzato nell'implementazione è OCaml. La scelta di utilizzare nuovamente OCaml semplifica l'integrazione nell'interfaccia del proof-checker. Inoltre, mentre le caratteristiche funzionali del linguaggio sono meno significative nell'ambito dello sviluppo di interfacce grafiche, il sofisticato sistema di type-inference unito alle feature object-oriented permettono di raggiungere elevati livelli di produttività e di correttezza e pulizia del codice.

Figura 7.1: Grafo delle dipendenze per i moduli dell'interfaccia Gtk

Pertanto, è stata scelta la divisione in moduli mostrata in figura 7.1, dove:

MmlInterface è il modulo radice, la cui interfaccia è vuota, che si occupa della gestione dei widget e delle finestre che compongono l'interfaccia grafica, invocando i (meta)moduli ProofChecker e XsltProcessor per le elaborazioni.

GtkMathView è il binding per OCaml del widget MathView, la cui interfaccia è⁵

exception ErrorLoadingFile of string
class math_view_signals :
  ([> `container | `widget | `math_view] as 'b) Gtk.obj ->
  object ('a)
    method jump :
      callback:(string -> unit) -> GtkSignal.id
  end
class math_view :
  Gtk_mathview.math_view Gtk.obj ->
  object
    method coerce : GObj.widget
    method connect : math_view_signals
    method get_selection : string option
    method load : filename:string -> unit
  end
val math_view :
  ?adjustmenth:GData.adjustment ->
  ?adjustmentv:GData.adjustment ->
  ?border_width:int ->
  ?width:int ->
  ?height:int ->
  ?packing:(GObj.widget -> unit) ->
  ?show:bool -> unit -> math_view

ProofChecker è il metamodulo logico comprendente tutti i moduli che compongono il proof-checker descritto nel capitolo 5.

XsltProcessor è il modulo che fornisce il binding per i processori XSLT e la cui interfaccia è:

  (* (process filename usecache mode) calls the XSLT      *)
  (* processor on the XML file whose name is filename.    *)
  (* mode could be either "theory" or "cic"               *)
  (* If usecache is true and the result of the processing *)
  (* is already in cache, then it is reused without       *)
  (* calling again the real XSLT processor.               *)
  process : string * bool * string -> string

Poiché è possibile effettuare il binding per OCaml esclusivamente di funzioni scritte in C e poiché tutti gli attuali processori XSLT sono scritti in Java, effettuare il binding per OCaml del codice Java è un'operazione complessa e prona ad errori. Inoltre, non è pensabile invocare ogni volta il processore XSLT da linea di comando, a causa del tempo richiesto per il bootstrap della Java Virtual Machine e l'elaborazione degli stylesheet. Pertanto, si è scelto di incapsulare i processori XSLT in demoni UDP e di implementare il modulo XsltProcessor in OCaml come un semplice client in grado di contattare tali demoni.

Figura 7.2: Protocollo di comunicazione fra il demone UDP con funzionalità di XSLT-processor e i client

In figura 7.2 viene mostrato il protocollo di comunicazione utilizzato fra il client e il demone: inputpath è il pathname del file XML al quale applicare le trasformazioni, outputpath è il pathname richiesto per il file XML ottenuto da tali applicazioni. Grazie all'idempotenza delle trasformazioni XSLT e al fatto che i file XML prodotti vengono mantenuti su disco fino alla chiusura dell'interfaccia, è possibile ottenere un protocollo fault-tolerant verso i guasti di comunicazione non bizantini semplicemente facendo reiterare la richiesta al client ad intervalli regolari fino a quando non riceve risposta, sotto il vincolo aggiuntivo che due richieste non possano mai differire esclusivamente per l'inputpath; grazie al precedente vincolo e all'utilizzo del disco come cache, nel caso che la stessa richiesta giunga nuovamente al server a causa di un guasto o dell'eccessiva lentezza di questo, l'overhead aggiuntivo consisterà esclusivamente nella rispedizione al client della conferma dell'avvenuta elaborazione.

L'unica critica alla precedente soluzione consiste nell'osservazione che, in tal modo, l'albero DOM ottenuto dalle trasformazioni XSLT deve essere serializzato su disco per poi essere nuovamente sottoposto a parsing dal widget MathView. Fino a quando il widget non esporrà un'interfaccia DOM (o equivalente) e potrà esclusivamente utilizzare file su disco come sorgenti, non ci saranno soluzioni alternative. Per questo motivo è prevista una futura estensione del widget al fine di dotarlo di tale funzionalità.

Seconda fase

Per trasformare l'interfaccia progettata nella prima fase in un prototipo per la (ri)annotazione dei termini è necessario:

Fornire una rappresentazione interna dei termini annotati e un cache per essi.
Fornire un parser per i file di annotazioni.
Fornire una funzione di salvataggio che, data la rappresentazione interna dei termini annotati, crei il file XML contenente le annotazioni.
Fornire un modulo che, data la rappresentazione interna di un termine annotato e dato un XPointer, ritorni il nodo selezionato dall'XPointer.
Fornire un modulo che, data la rappresentazione interna di un termine e il riferimento ad uno dei nodi, ritorni la lista dei suggerimenti da utilizzare per annotare tale nodo.

In questa fase, l'obiettivo non è quello di sviluppare un vero tool per l'annotazione, ma esclusivamente quello di capire se un tale tool sia realizzabile e quale sia la sua utilità (programmazione esplorativa). Pertanto, la fase di progettazione è stata ridotta al minimo e si è deciso, una volta capite le funzionalità necessarie, di abbandonare il prototipo e ricominciare dalla fase di specifica. In questo lavoro, quindi, non viene riportata la strutturazione in moduli del prototipo, nè le loro interfacce, ancora soggette a cambiamenti continui. Indicativamente, comunque:

Per quanto riguarda i punti 1 e 2, al modulo Cic già sviluppato per il proof-checker è stata aggiunta la nuova rappresentazione interna e sono stati modificati per utilizzarla sia il metamodulo CicParser che il modulo CicCache.
Per implementare le funzioni dei punti 3 e 4 sono stati creati due nuovi moduli, chiamati rispettivamente Cic2Xml e CicXPath, che espongono ognuno una sola funzione e le cui interfacce sono ovvie. Il modulo CicXPath riconosce esclusivamente il sottoinsieme banale di XPath effettivamente utilizzato in HELM.
Per implementare il punto 5 è stato creato un ulteriore modulo che espone una sola funzione che restituisce come suggerimenti una lista ordinata di stringhe di markup XML da associare ai pulsanti della palette.

7.2.2 Risultati ottenuti

Per quanto riguarda le funzionalità di proof-checking e resa, l'interfaccia ha dato risultati incoraggianti: grazie all'utilizzo delle usuali notazioni matematiche, della rappresentazione ad albero della libreria, della presenza di collegamenti ipertestuali e dell'utilizzo del prototipo di generazione automatica della descrizione in linguaggio naturale della prova, gli oggetti della libreria standard di Coq possono essere finalmente piacevolmente usufruiti⁶, anche se l'interpretazione della maggior parte delle prove è ancora un'operazione complessa, riservata ai conoscitori del sistema logico.

Per quanto riguarda l'utilizzo dell'interfaccia come prototipo per la (ri)annotazione delle prove, i risultati ottenuti indicano chiaramente la necessità di ristrutturare alcune delle componenti sviluppate in precedenza. Infatti, nonostante il meccanismo dei suggerimenti risulti promettente, la riannotazione di un termine è resa estremamente penosa dalla necessità, ad ogni modifica, di esportare su file la nuova notazione, riapplicare le trasformazioni presentazionali e riprocessare con il widget il risultato ottenuto; complessivamente, queste operazioni possono richiedere ogni volta anche alcuni minuti.

Per risolvere questo problema è necessario:

Ristrutturare gli stylesheet in modo che sia possibile applicarli ad un sotto-termine.
Dotare il widget di un'interfaccia DOM o equivalente che permetta la modifica di una sotto-espressione.
Riprogettare il prototipo in modo da utilizzare i precedenti meccanismi.

1: http://xml.apache.org
2: Xalan-C è il porting in C++ del processore Xalan-J sviluppato nell'ambito dell'Apache XML Project e attualmente utilizzato da Cocoon nei siti di presentazione del progetto HELM.
3: Al momento, le teorie vengono rese giustapponendo la rappresentazione dei singoli oggetti che le compongono.
4: Gli hyperlink sono collegamenti conformi allo standard XLink introdotti durante le trasformazioni dal formato del sistema logico a quello content e successivamente propagati nella successiva trasformazione. Non sono ancora riconosciuti dai browser standard e, pertanto, non sono ancora usufruibili usando la precedente interfaccia.
5: Vengono riportati solamente i metodi effettivamente utilizzati, tranne quelli ereditati dalla superclasse GContainer.container, che vengono tutti omessi.
6: A patto di essere pazienti! Poiché viene utilizzato lo stesso processore XSLT usato con Cocoon, le prestazioni sono deludenti per le stesse motivazioni esposte a pagina 7.1.1.