helm/gTopLevel/TATTICHE

   1 V7.2:
   2
   3 Da valutare:
   4  * MetaLinguaggio di David Delayale per l'implementazione di tattiche
   5
   6 V6.3:
   7
   8 Da valutare:
   9  * Print
  10  * Extraction
  11  * Opaque/Transparent
  12  * SearchIsos
  13  * Load di script di tattiche
  14  * "Pretty" Parsing
  15  * Log dei tempi per ogni possibile richiesta
  16  * Undo
  17  * Focus/Unfocus (nella prova completa in linguaggio naturale)
  18  * Show Tree (resa dell'albero dei sequenti)
  19  * Tatticali:
  20     - OrElse
  21     - Repeat
  22     - Do
  23     - Info
  24     - Try
  25     - First
  26     - Solve
  27     - Abstract
  28     - ;
  29     - ; [ ... | ... | ... ]
  30     - (...)
  31  * Assumption
  32  * Apply with
  33  * LApply
  34  * Absurd
  35  * Contradiction
  36  * Cbv/Lazy Beta Delta Iota Zeta
  37  * Red (riduzione di un backbone con delta della testa + beta e iota)
  38  * Unfold (equivalente a Hnf dell'occorrenza)
  39  * Pattern
  40  * Constructor n / Split / Left/ Right/ Exists/ Reflexivity
  41  * Elim term quando term ha come tipo un Pi
  42  * ElimType (fatta da Zack; metterla disponibile)
  43  * Induction su una applicazione
  44  * Induction su una ipotesi
  45  * Case su una applicazione e su una ipotesi
  46  * Intros destrutturante
  47  * Decompose
  48  * Double Induction
  49  * Rewrite (ma eliminare un'uguaglianza o applicare eq_ind_r non funziona gia'?)
  50  * Replace (che prende due termini _NON_ convertibili e genera come goal
  51    l'uguaglianza dei due). Unificarla con la change, che diventa la replace
  52    non overkilling?
  53  * Symmetry e Transitivity (basta applicare i due teoremi giusti)
  54  * Decide Equality (ma non dovrebbe essere un teorema???)
  55  * Compare
  56  * Discriminate
  57  * Injection
  58  * Simplify_eq (== Discriminate o Injection su una ipotesi)
  59  * Dependent Rewrite
  60  * Inversion [Nota: Derive Inversion genera e salva il teorema!]
  61  * Quote (per implementare tattiche riflessive senza scrivere codice ML!!!!)
  62  * Tauto/Intuition
  63  * Linear
  64  * AutoRewrite
  65  * Realizer/Program
  66  * Scheme
  67  * Omega
  68
  69 Implementate:
  70  * Enunciare un teorema
  71  * (Ri)aprire un teorema gia' dimostrato per modificarne certe parti
  72  * Check (e successiva possibilita' di applicare reduction tactics)
  73  * Exact
  74  * Apply/EApply
  75  * Cut
  76  * Change [Una conversion tactic. Problema: il termine digitato viene
  77     parsato nel contesto della conclusione e non in quello della selezione!!!]
  78  * Conversion tactics, sia nelle ipotesi che nella conclusione:
  79    - Reduce (== Compute)
  80    - Hnf
  81    - Simpl
  82  * Fold
  83  * ElimIntrosSimpl
  84  * Let...In (= LetTac)
  85  * Salvare e caricare una prova incompleta (ma nel posto sbagliato!)
  86  * ClearBody
  87  * Clear
  88  * Ring
  89
  90 Da implementare:
  91  * Implicit: quando si usano gli implicit, l'input non puo' piu' essere
  92    type-checkato, ma bisogna fare una refine (ancora non implementata).
  93    Di conseguenza _OGNI_ tattica si rompe. Inoltre l'implementazione di
  94    Implicit e' ancora errata in quanto il contesto canonico delle nuove
  95    variabili e' sempre vuoto anche se dovrebbe essere uguale a quello
  96    di partenza + le nuove variabili introdotte durante il parsing.
  97  * Nella type_of NON viene controllato che il metasenv di una current-proof
  98    sia ben formato. PUNTO IMPORTANTE: farlo nel metasenv parziale, cosi' da
  99    evitare cicli; ma dopo e' un bordello l'unificazione. Oppure fare un
 100    semplice controllo di aciclicita'.
 101  * ClearBody e Clear NON restringono ancora altre metavariabili. Invece viene
 102    sollevata un'eccezione di tipaggio. Esempio: n:nat |- ?1[n] se faccio clear
 103    di n dovrei restringere ?1. Se invece prima faccio clear di n in ?1, quando
 104    torno su questo goal e faccio clear di n ottengo un'eccezione di CicPp.
 105  * La reduction_tactic (in ProofEngine.ml) e' bacatissima, come descritto
 106    nei commenti. Fixare.
 107  * Reimplementare Cut usando LetIn + applicazione + Intro oppure usando
 108    LetIn + ClearBody (soluzione piu' elegante IMHO)
 109  * Refine
 110  ? Sia [x:=t]r il tipo di [x:t]k e x non occorra mai libera in r.
 111    Dovrei forse tornare semplicemente r?
 112  ? Cambiare il nome delle META da int a una stringa?
 113    [ATTENZIONE: CAMBIAMENTO NELLA DTD]
 114  * Fold e' l'inverso di Reduce e quindi non disfa cio' che viene fatto da
 115    Simpl e da Whd. Generalizzarlo facendo Reduce e poi Change con ogni termine?
 116    Oppure fare una FoldWhd, una FoldHnf, una FoldSimpl, etc.?
 117  * Fold localizzato in un termine selezionato
 118  * Move e "Unclear" (che fa l'undo di Clear/Move e conversioni nelle ipotesi)
 119    Non sono implementabili. Ma avrebbero senso?
 120  * queries e roba basata sulle queries:
 121    - Search
 122    - Locate (anche di tipi induttivi e costruttori)
 123    - Auto
 124    - EAuto
 125    - Prolog (???????????)
 126  * Save con tanto di esportazione: esportare nel posto giusto!
 127  * Dare una definizione (quasi equivalente a check + unfold, ma mancano
 128    gli inner-types)
 129  * Dare una definizione induttiva
 130  * Intro (Come scegliere i nomi freschi?) e Intros until
 131  * Generalize
 132  * Fissare il bug di change (ovvero il problema del contesto in cui viene
 133    parsato l'input dell'utente)
 134  * Tornare un errore se si cerca di applicare una reduction tactic in una
 135    ipotesi nella scratch area
 136  * Field
 137  * JProver. Che rapporto c'e' fra JProver e Tauto/Intuition?
 138  * altre contrib da integrare?
 139
 140 Da non implementare:
 141   * Print All
 142   * Compile/Read/Require
 143   * Print/Save/Restore States
 144   * Let