+++ /dev/null
-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
projects / helm.git / blobdiff