X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=3d272d3781049920166deca55164083e7c07aa24;hb=e7916b85dd9dab26b628ace838c683beb31db9c1;hp=05c28af47aaf62196e88b952518b9b0cbe6952db;hpb=6b8da04f526b3484dc92f61a23a8e61e63422c13;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 05c28af47..3d272d378 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,15 +2,40 @@ (**********************************************************************) TODO -- implementare macro in matitaScript.ml (check, hint, ..) -> Gares -- script outline -> Zack +- elim_intros_simpl e rewrite_simpl: ora non viene usata dal + ^^^^^^ ^^^^^^ + toplevel la variante che semplifica. Capire quali sono i problemi + e/o cosa fare delle varianti con semplificazione. +- eta_expand non usata da nessuno? +- eliminare eta_fix? (aspettare notazione da Zack e Luca) +- bug di ferruccio: fare un refresh dei nomi dopo l'applicazione + di una tattica. Di quali nomi fare refresh? (Andrea) di quelli + veramente ambigui, ovvero dell'ultimo binder tale che sotto di + esso un nome viene usato in maniera ambigua. Esempio: + \lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh + \lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh +- a volte genera termini con variabili legate da piu' binder + Capita quando un tipo dall'environment (e.g. \lambda x.T) + viene inserito in un contesto (e.g. x:nat) dove le variabili + sono gia' state legate in precedenza. +- script outline -> Zack - cicBrowser: riagganciare(?) resa di termini scritti - nella URL(??) -> -- menu contestuale (tasto dx) nel sequent viewer -> -- controllo per script modificato o meno prima di uscire -> -- riattaccare hbugs (brrr...) -> Zack + nella URL(??) -> +- menu contestuale (tasto dx) nel sequent viewer -> +- riattaccare hbugs (brrr...) -> Zack DONE +- controllo per script modificato o meno prima di uscire -> Gares +- LApply deve prendere in input gli identificatori che va a generare; + lascio a Ferruccio la scelta della sintassi concreta -> Ferruccio +- fare tornare a matitac -1 quando lo stato finale e' + diverso da No_proof, non eseguire comandi quando lo + stato e' diverso da No_proof -> CSC +- uri_of_term and term_of_uri: cambiare il tipo per far + tornare delle uri!!! -> CSC +- intro = intros 1 -> Gares +- timetravel (urimanager) -> Gares +- implementare macro in matitaScript.ml -> Gares - history deve aggiornare anche la whelp bar -> Gares - commenti exeguibili (forse devono essere una lista e non un singolo executable e forse devono contenere anche Note @@ -18,20 +43,20 @@ DONE - spostare il codice di creazione delle tabelle da MatitaDb, al momento quelle create da matita possono andare out of sync con quelle create dai file .sql -> Gares -- tree update in background -> Gares -- update del getter in background -> Zack -- agganciare href_callback del sequent_viewer -> Zack -- shortcut varie per script handling -> Zack -- operazioni rimanenti su script (top, bottom, jump) -> Zack -- lighting-ls-getter in matita -> Gares -- riagganciare toolbar -> Zack +- tree update in background -> Gares +- update del getter in background -> Zack +- agganciare href_callback del sequent_viewer -> Zack +- shortcut varie per script handling -> Zack +- operazioni rimanenti su script (top, bottom, jump) -> Zack +- lighting-ls-getter in matita -> Gares +- riagganciare toolbar -> Zack - evitare che n-mila tattiche Goal siano nello script - (una per ogni cambio di tab) -> Zack -- implementazione comandi rimanenti in matitaEngine.ml -> Gares -- sintassi per gli alias -> Gares -- implementazione script handling (sopra engine) -> Zack + (una per ogni cambio di tab) -> Zack +- implementazione comandi rimanenti in matitaEngine.ml -> Gares +- sintassi per gli alias -> Gares +- implementazione script handling (sopra engine) -> Zack - matitaSync all'indietro -> Gares -- riagganciare GUI -> Zack +- riagganciare GUI -> Zack (**********************************************************************) @@ -56,9 +81,9 @@ comandi: | lingua:/sintassi concreta non ambigua delle tattiche+Qed,Thm,alias/ +---------------------------------------------------------- | engine: TacticAst (cic) -> status -> status - | ma non usa il campo alias dello status + | ma non usa il campo alias dello status ---------+---------------------------------------------------------- - ocaml + ocaml -------------------------------------------------------------------- @@ -137,33 +162,33 @@ script handling - new: gtk_text_buffer -> script - redraw: unit (* ridisegna il contenuto del buffer di testo *) - advance: ?statement:string -> unit -> unit - (* valuta il primo statement del future text (usando eval_statement - (puo' fallire con una eccezione)), rimuove il testo corrispondente dal - future text, aggiunge alla statement list una entry per ogni statement - ritornato da eval_statement, aggiunge il nuovo stato alla state list, - invoka tutti gli observer - Se c'e' l'argomento opzionale statement, quello e' il testo che viene - passato ad eval_statement, se ha successo nessuna rimozione dal future - text viene effettuata *) + (* valuta il primo statement del future text (usando eval_statement + (puo' fallire con una eccezione)), rimuove il testo corrispondente dal + future text, aggiunge alla statement list una entry per ogni statement + ritornato da eval_statement, aggiunge il nuovo stato alla state list, + invoka tutti gli observer + Se c'e' l'argomento opzionale statement, quello e' il testo che viene + passato ad eval_statement, se ha successo nessuna rimozione dal future + text viene effettuata *) - retract: unit -> unit - (* sposta l'ultimo statement della statement list al future text, toglie - l'ultimo stato della state list, MatitaSync.time_travel - ~present:ultimo_stato ~past:stato_precedente *) + (* sposta l'ultimo statement della statement list al future text, toglie + l'ultimo stato della state list, MatitaSync.time_travel + ~present:ultimo_stato ~past:stato_precedente *) - private eval_statement: string -> MatitaTypes.status * string list - (* parsa lo statement - - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine - passando lo stato corrente - - se e' una Macro la gestisce (= tutte le Macro sono implementate qua) - Ritorna una lista di coppie . La proiezione sulla - prima componente rappresenta gli stati da aggiungere alla state list; - quella sulla seconda gli statement da aggiungere alla statement list. - *) + (* parsa lo statement + - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine + passando lo stato corrente + - se e' una Macro la gestisce (= tutte le Macro sono implementate qua) + Ritorna una lista di coppie . La proiezione sulla + prima componente rappresenta gli stati da aggiungere alla state list; + quella sulla seconda gli statement da aggiungere alla statement list. + *) (* gestione degli observer *) - add_observer: (MatitaTypes.status -> unit) -> observer_id - remove_observer: observer_id -> unit (* gestione del salvataggio *) - - save_to: string -> unit (* ridisegna su file *) + - save_to: string -> unit (* ridisegna su file *) - load_from: string -> unit (* retract fino allo stato zero, nuovo stato con future text pari al - contenuto del file passato *) + contenuto del file passato *)