X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2FTATTICHE;fp=helm%2FgTopLevel%2FTATTICHE;h=0000000000000000000000000000000000000000;hp=88d989ded241cd3c01920b39dd761eb2f8a985dc;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/gTopLevel/TATTICHE b/helm/gTopLevel/TATTICHE
deleted file mode 100644
index 88d989ded..000000000
--- a/helm/gTopLevel/TATTICHE
+++ /dev/null
@@ -1,144 +0,0 @@
-V7.2:
-
-Da valutare:
- * MetaLinguaggio di David Delayale per l'implementazione di tattiche
-
-V6.3:
-
-Da valutare:
- * Print
- * Extraction
- * Opaque/Transparent
- * SearchIsos
- * Load di script di tattiche
- * "Pretty" Parsing
- * Log dei tempi per ogni possibile richiesta
- * Undo
- * Focus/Unfocus (nella prova completa in linguaggio naturale)
- * Show Tree (resa dell'albero dei sequenti)
- * Tatticali:
-    - OrElse
-    - Repeat
-    - Do
-    - Info
-    - Try
-    - First
-    - Solve
-    - Abstract
-    - ;
-    - ; [ ... | ... | ... ]
-    - (...)
- * Assumption
- * Apply with
- * LApply
- * Absurd
- * Contradiction
- * Cbv/Lazy Beta Delta Iota Zeta
- * Red (riduzione di un backbone con delta della testa + beta e iota)
- * Unfold (equivalente a Hnf dell'occorrenza)
- * Pattern
- * Constructor n / Split / Left/ Right/ Exists/ Reflexivity
- * Elim term quando term ha come tipo un Pi
- * ElimType (fatta da Zack; metterla disponibile)
- * Induction su una applicazione
- * Induction su una ipotesi
- * Case su una applicazione e su una ipotesi
- * Intros destrutturante
- * Decompose
- * Double Induction
- * Rewrite (ma eliminare un'uguaglianza o applicare eq_ind_r non funziona gia'?)
- * Replace (che prende due termini _NON_ convertibili e genera come goal
-   l'uguaglianza dei due). Unificarla con la change, che diventa la replace
-   non overkilling?
- * Symmetry e Transitivity (basta applicare i due teoremi giusti)
- * Decide Equality (ma non dovrebbe essere un teorema???)
- * Compare
- * Discriminate
- * Injection
- * Simplify_eq (== Discriminate o Injection su una ipotesi)
- * Dependent Rewrite
- * Inversion [Nota: Derive Inversion genera e salva il teorema!]
- * Quote (per implementare tattiche riflessive senza scrivere codice ML!!!!)
- * Tauto/Intuition
- * Linear
- * AutoRewrite
- * Realizer/Program
- * Scheme
- * Omega
-
-Implementate:
- * Enunciare un teorema
- * (Ri)aprire un teorema gia' dimostrato per modificarne certe parti
- * Check (e successiva possibilita' di applicare reduction tactics)
- * Exact
- * Apply/EApply
- * Cut
- * Change [Una conversion tactic. Problema: il termine digitato viene
-    parsato nel contesto della conclusione e non in quello della selezione!!!]
- * Conversion tactics, sia nelle ipotesi che nella conclusione:
-   - Reduce (== Compute)
-   - Hnf
-   - Simpl
- * Fold
- * ElimIntrosSimpl
- * Let...In (= LetTac)
- * Salvare e caricare una prova incompleta (ma nel posto sbagliato!)
- * ClearBody
- * Clear
- * Ring
-
-Da implementare:
- * Implicit: quando si usano gli implicit, l'input non puo' piu' essere
-   type-checkato, ma bisogna fare una refine (ancora non implementata).
-   Di conseguenza _OGNI_ tattica si rompe. Inoltre l'implementazione di
-   Implicit e' ancora errata in quanto il contesto canonico delle nuove
-   variabili e' sempre vuoto anche se dovrebbe essere uguale a quello
-   di partenza + le nuove variabili introdotte durante il parsing.
- * Nella type_of NON viene controllato che il metasenv di una current-proof
-   sia ben formato. PUNTO IMPORTANTE: farlo nel metasenv parziale, cosi' da
-   evitare cicli; ma dopo e' un bordello l'unificazione. Oppure fare un
-   semplice controllo di aciclicita'.
- * ClearBody e Clear NON restringono ancora altre metavariabili. Invece viene
-   sollevata un'eccezione di tipaggio. Esempio: n:nat |- ?1[n] se faccio clear
-   di n dovrei restringere ?1. Se invece prima faccio clear di n in ?1, quando
-   torno su questo goal e faccio clear di n ottengo un'eccezione di CicPp.
- * La reduction_tactic (in ProofEngine.ml) e' bacatissima, come descritto
-   nei commenti. Fixare.
- * Reimplementare Cut usando LetIn + applicazione + Intro oppure usando
-   LetIn + ClearBody (soluzione piu' elegante IMHO)
- * Refine
- ? Sia [x:=t]r il tipo di [x:t]k e x non occorra mai libera in r.
-   Dovrei forse tornare semplicemente r?
- ? Cambiare il nome delle META da int a una stringa?
-   [ATTENZIONE: CAMBIAMENTO NELLA DTD]
- * Fold e' l'inverso di Reduce e quindi non disfa cio' che viene fatto da
-   Simpl e da Whd. Generalizzarlo facendo Reduce e poi Change con ogni termine?
-   Oppure fare una FoldWhd, una FoldHnf, una FoldSimpl, etc.?
- * Fold localizzato in un termine selezionato
- * Move e "Unclear" (che fa l'undo di Clear/Move e conversioni nelle ipotesi)
-   Non sono implementabili. Ma avrebbero senso?
- * queries e roba basata sulle queries:
-   - Search
-   - Locate (anche di tipi induttivi e costruttori)
-   - Auto
-   - EAuto
-   - Prolog (???????????)
- * Save con tanto di esportazione: esportare nel posto giusto!
- * Dare una definizione (quasi equivalente a check + unfold, ma mancano
-   gli inner-types)
- * Dare una definizione induttiva
- * Intro (Come scegliere i nomi freschi?) e Intros until
- * Generalize
- * Fissare il bug di change (ovvero il problema del contesto in cui viene
-   parsato l'input dell'utente)
- * Tornare un errore se si cerca di applicare una reduction tactic in una
-   ipotesi nella scratch area
- * Field
- * JProver. Che rapporto c'e' fra JProver e Tauto/Intuition?
- * altre contrib da integrare?
-
-Da non implementare:
-  * Print All
-  * Compile/Read/Require
-  * Print/Save/Restore States
-  * Let