helm/matita/matita.txt

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