helm/matita/matita.txt

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