helm/matita/matita.txt

   1
   2 (**********************************************************************)
   3
   4 TODO
   5 - preoccupante: per
   6   inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
   7   noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero
   8   essere accettati dal nostro nucleo che invece non fa una piega!!!)
   9 - parsing contestuale (tattiche replace, change e forse altre)
  10 - assiomi
  11 - Guardare il commento
  12   (*CSC: this code is suspect and/or bugged: we try first without reduction
  13   and then using whd. However, the saturate_term always tries with full
  14   reduction without delta. *)
  15   in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply
  16   oltre che di bug!
  17 - Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
  18   lockato!
  19 - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
  20   finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
  21   codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
  22 - quando si sposta il punto di esecuzione dello script cambiare la parte di
  23   script visibile nella finestra dello script
  24 - Dare errore significativo al posto di NotWellTypedInterpreation
  25 - Implementare menu edit: find/replace/cut/copy/undo/etc.
  26 - Bug vari nella generazione dei principi di eliminazione:
  27    1. generazione nomi (usa ref incrementata localmente)
  28    2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
  29       passo il test inversion.ma)
  30    3. usato trucco outtype non dipendenti per il case
  31 - elim_intros_simpl e rewrite_simpl: ora non viene usata dal
  32              ^^^^^^           ^^^^^^
  33   toplevel la variante che semplifica. Capire quali sono i problemi
  34   e/o cosa fare delle varianti con semplificazione.
  35 - eta_expand non usata da nessuno?
  36 - notazione -> Luca e Zack
  37 - eliminare eta_fix? (aspettare notazione)
  38 - bug di refresh del widget quando si avanza ("swap" tra la finestra dei
  39   sequenti e la finestra dello script)
  40 - feedback su hyperlink nei sequenti e nel browser: rendere visibili gli
  41   hyperlink (cursore a "manina"? hyperlink evidenziati?). La maction che
  42   collassa la prova e' fastidiosa: la prova si chiude se non si clicca
  43   correttamente su un hyperlink
  44 - disabilitare (set_sensitive false) menu e bottoni mentre matita sta
  45   processando lo script per evitare interazioni pericolose
  46 - bug di ferruccio: fare un refresh dei nomi dopo l'applicazione
  47   di una tattica. Di quali nomi fare refresh? (Andrea) di quelli
  48   veramente ambigui, ovvero dell'ultimo binder tale che sotto di
  49   esso un nome viene usato in maniera ambigua. Esempio:
  50   \lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh
  51   \lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh
  52 - a volte genera termini con variabili legate da piu' binder
  53   Capita quando un tipo dall'environment (e.g. \lambda x.T)
  54   viene inserito in un contesto (e.g. x:nat) dove le variabili
  55   sono gia' state legate in precedenza.
  56 - script outline -> Zack
  57 - cicBrowser: riagganciare(?) resa di termini scritti
  58   nella URL(??)
  59 - menu contestuale (tasto dx) nel sequent viewer -> attende notazione
  60 - riattaccare hbugs (brrr...)                             -> Zack
  61 - gestione dei path per include: il path deve essere assoluto? da decidere ...
  62 - highlight degli errori di parsing nello script (usando lo sfondo come per la
  63   parte lockata di testo, da ripulire quando si modifica il testo o si sposta il
  64   punto di esecuzione)
  65 - salvare la parte di testo lockata dagli effetti di undo/redo (come?????)
  66 - supportare l'apertura di piu' script contemporaneamente in tab/finestre
  67   diversi/e
  68
  69 DONE
  70 - controllo per script modificato o meno prima di uscire  -> Gares
  71 - LApply deve prendere in input gli identificatori che va a generare;
  72   lascio a Ferruccio la scelta della sintassi concreta    -> Ferruccio
  73 - fare tornare a matitac -1 quando lo stato finale e'
  74   diverso da No_proof, non eseguire comandi quando lo
  75   stato e' diverso da No_proof                            -> CSC
  76 - uri_of_term and term_of_uri: cambiare il tipo per far
  77   tornare delle uri!!!                                    -> CSC
  78 - intro = intros 1                                        -> Gares
  79 - timetravel (urimanager)                                 -> Gares
  80 - implementare macro in matitaScript.ml                   -> Gares
  81 - history deve aggiornare anche la whelp bar              -> Gares
  82 - commenti exeguibili (forse devono essere una lista e non
  83   un singolo executable e forse devono contenere anche Note
  84   e non solo Executable)                                  -> Gares
  85 - spostare il codice di creazione delle tabelle da
  86   MatitaDb, al momento quelle create da matita possono
  87   andare out of sync con quelle create dai file .sql      -> Gares
  88 - tree update in background                               -> Gares
  89 - update del getter in background                         -> Zack
  90 - agganciare href_callback del sequent_viewer             -> Zack
  91 - shortcut varie per script handling                      -> Zack
  92 - operazioni rimanenti su script (top, bottom, jump)      -> Zack
  93 - lighting-ls-getter in matita                            -> Gares
  94 - riagganciare toolbar                                    -> Zack
  95 - evitare che n-mila tattiche Goal siano nello script
  96   (una per ogni cambio di tab)                            -> Zack
  97 - implementazione comandi rimanenti in matitaEngine.ml    -> Gares
  98 - sintassi per gli alias                                  -> Gares
  99 - implementazione script handling (sopra engine)          -> Zack
 100 - matitaSync all'indietro                                 -> Gares
 101 - riagganciare GUI                                        -> Zack
 102
 103 (**********************************************************************)
 104
 105 comandi:
 106  - interattivi (solo da gui)
 107    - Macro/Comandi (check, print, hint, undo, locate, match)
 108      potrebbero anche non avere sintassi concreta, del tipo che
 109      check e' solo un bottone che apre una finetra in cui puoi
 110      scrivere un termine o selezionarlo dalla prova corrente
 111  - batch (sono gli unici che stanno nel .ma)
 112    - Tattiche, theorem, alias (cambiano la prova)
 113
 114
 115           MOUSE
 116 -------------------------------------------+
 117  gui (macro: hint)                         |      SHELL
 118      (disambiguatore)                      |
 119          +-----------------+---------------+-----------------------------------
 120          | matita (status) |               | matitac
 121          | (log) (sync)    |    but2log    | fold ( fun s l -> engine l s) file
 122          +-----------------+---------------+-----------------------------------
 123          |  lingua:/sintassi concreta non ambigua delle tattiche+Qed,Thm,alias/
 124          +----------------------------------------------------------
 125          |            engine: TacticAst (cic) -> status -> status
 126          |               ma non usa il campo alias dello status
 127 ---------+----------------------------------------------------------
 128                             ocaml
 129 --------------------------------------------------------------------
 130
 131
 132 engine:
 133  - accetta solo linee non ambigue
 134  - alias:
 135      alias ident nat = "cic:/matita/gares/nat.ind#(1/1)".
 136      alias number = (natural|real|positive|integer).
 137
 138
 139
 140 matita:
 141  - mantiene uno stack di stati
 142  - mantiene un log sync con gli stati
 143  - offre delle api per generare la sintassi concreta che puo' servire
 144    alla gui (la gui fa una chiamata a funzione e matita genera "auto."
 145    cosi' la sintassi la gui non la vede mai e la tratta al massimo come un
 146    testo semplice e basta (insomma, metterei in matita il generatore di
 147    sintassi concreta) but2log
 148  - ha il controllo... ovvero anche la gui viene usata da matita, o per sapere
 149    la prossima azione o per chidere di scegliere il termine tra una lista
 150
 151  (stato :: tl) (log , (start,end) :: tl)
 152
 153  +----------+
 154  |          |
 155  +----------+
 156
 157 gui:
 158  - step
 159  - choose
 160
 161 stato:
 162  - alias
 163  - proof status option
 164  - metadati relativi allo script per il sync
 165  - settings "baseuri/url/" eccc
 166  -
 167
 168 alias
 169  - sintassi concreta
 170
 171 engine prende in input
 172  - AST di Cic (tactic ast)
 173
 174 sync:
 175  - presi 2 stati fa il diff e lo somma/sottrae al DB
 176
 177 (**********************************************************************)
 178
 179 script handling
 180 - ad ogni script sul quale l'utente sta lavorando corrispondono
 181   - un modello (vedi sotto)
 182   - un buffer di testo gtk + attributi (usati principalmente per distinguere la
 183     parte di testo immodificabile da quella modificabile)
 184   - una lista di observer che vengono notificati ad ogni cambiamento di stato
 185 - un modello di script e' composto da:
 186   - una lista di stringhe (inizialmente vuota) detta "statement list". Ogni
 187     elemento della lista corrisponde ad uno statement (nel senso di
 188     TacticAst.statement) gia' valutato dall'engine. La parte immodificabile del
 189     buffer di testo corrisponde con le stringhe contenute nella lista
 190   - una lista di stati (inizialmente contenente lo stato vuoto) detta "state
 191     list". Si ha l'invariante che la lunghezza di tale lista e' uguale alla
 192     lunghezza della statements list + 1. Lo stato i-esimo della lista di stati
 193     e' lo stato di matita _prima_ dell'esecuzione dell i-esimo statement
 194   - una stringa, detta "future text", corrispondente alla parte di testo dello
 195     script non ancora valutata. L'ultimo stato della state list e' lo stato
 196     corrente di matita
 197 - relazione tra modello e buffer di testo gtk
 198   - le modifiche al testo del buffer sono possibili solo nella parta non ancora
 199     valutata. Ognuna di esse viene apportata _anche_ al future text
 200   - invariante: e' sempre possibile riscrivere ("redraw") l'intero contenuto del
 201     buffer di testo a partire dal modello, attributi compresi
 202 - oggetto script
 203   - metodi
 204     - new: gtk_text_buffer -> script
 205     - redraw: unit (* ridisegna il contenuto del buffer di testo *)
 206     - advance: ?statement:string -> unit -> unit
 207         (* valuta il primo statement del future text (usando eval_statement
 208         (puo' fallire con una eccezione)), rimuove il testo corrispondente dal
 209         future text, aggiunge alla statement list una entry per ogni statement
 210         ritornato da eval_statement, aggiunge il nuovo stato alla state list,
 211         invoka tutti gli observer
 212         Se c'e' l'argomento opzionale statement, quello e' il testo che viene
 213         passato ad eval_statement, se ha successo nessuna rimozione dal future
 214         text viene effettuata *)
 215     - retract: unit -> unit
 216         (* sposta l'ultimo statement della statement list al future text, toglie
 217         l'ultimo stato della state list, MatitaSync.time_travel
 218         ~present:ultimo_stato ~past:stato_precedente *)
 219     - private eval_statement: string -> MatitaTypes.status * string list
 220         (* parsa lo statement
 221         - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine
 222           passando lo stato corrente
 223         - se e' una Macro la gestisce (= tutte le Macro sono implementate qua)
 224           Ritorna una lista di coppie <stato, statement>. La proiezione sulla
 225           prima componente rappresenta gli stati da aggiungere alla state list;
 226           quella sulla seconda gli statement da aggiungere alla statement list.
 227         *)
 228     (* gestione degli observer *)
 229     - add_observer: (MatitaTypes.status -> unit) -> observer_id
 230     - remove_observer: observer_id -> unit
 231     (* gestione del salvataggio *)
 232     - save_to: string -> unit        (* ridisegna su file *)
 233     - load_from: string -> unit
 234         (* retract fino allo stato zero, nuovo stato con future text pari al
 235         contenuto del file passato *)
 236