From 4545d7dd07b44b0a755d516bef082b6a1a83ec24 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 8 Sep 2005 11:55:16 +0000 Subject: [PATCH] items related to lazy parsing --- helm/matita/matita.txt | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 00290751c..478cd77ab 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -11,29 +11,14 @@ TODO TATTICHE + - verificare il comportamento di tutte le tattiche con il parsing lazy -> CSC - file elim.ma: vengono creati lambda dummy e referenziati nell'outtype di un case - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire - comportamento di tutte le tattiche nei confronti dei let-in - - tattica unfold su rel a let-in bound variables: c'e' ancora un bug - aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto - del goal e non in quello del pattern. Pertanto invece di cercare di - fare unfolding di x viene fatto unfolding di altro. - Soluzione: la funzione ProofEngineHelpers.select deve tornare una - funzione per rilocare i termini nel contesto giusto. - Esempio: - theorem t: let uno \def S O in uno + uno = S uno \to uno=uno. - intros. unfold uno in H. - NOTA: questo bug e' legato a quello di parsing in presenza di tattiche - con pattern, visto che in tal caso e' l'intero parsing a dover essere - fatto in un contesto differente. Risolvendo quel bug si risolve - automaticamente anche questo. - elim con pattern - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con True. - - parsing contestuale (tattiche replace, change e forse altre) - capire dove fare la select per avere i contesti in cui disambiguare gli - altri argomenti. - assiomi (manca sintassi concreta e AST). - Guardare il commento (*CSC: this code is suspect and/or bugged: we try first without reduction @@ -128,6 +113,23 @@ TODO DEMONI E ALTRO DONE +- parsing contestuale (tattiche replace, change e forse altre) + capire dove fare la select per avere i contesti in cui disambiguare gli + altri argomenti. -> Zack, Enrico, CSC +- tattica unfold su rel a let-in bound variables: c'e' ancora un bug + aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto + del goal e non in quello del pattern. Pertanto invece di cercare di + fare unfolding di x viene fatto unfolding di altro. + Soluzione: la funzione ProofEngineHelpers.select deve tornare una + funzione per rilocare i termini nel contesto giusto. + Esempio: + theorem t: let uno \def S O in uno + uno = S uno \to uno=uno. + intros. unfold uno in H. + NOTA: questo bug e' legato a quello di parsing in presenza di tattiche + con pattern, visto che in tal caso e' l'intero parsing a dover essere + fatto in un contesto differente. Risolvendo quel bug si risolve + -> Zack, Enrico, CSC + automaticamente anche questo. - Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack - implementare inclusione file di configurazione (perche' ora tutti -- 2.39.2