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