Write a dependently typed interpreter for a simple programming language with ML-style pattern-matching.
The object language is defined informally by this grammar:
t ::= bool | t + t
p ::= x | b | inl p | inr p
e ::= x | b | inl e | inr e | case e of [p ⇒ e]* [_ ⇒ e]
The non-terminal x stands for a variable, and b stands for a boolean constant. The
production for case expressions means that a pattern-match includes zero or more
pairs of patterns and expressions, and a default case. The sum type t1 + t2 has cannonical values inl e1, where e1 has type t1 and inr e2, where e2 has type t2. This means (surprize! surprize!) that it is identical to the Coq sum operator.
Your interpreter should be implemented in the style demonstrated in chapter 9 (Section 9.2.1 in particular). That
is, your definition of expressions should use dependent types and de Bruijn indices to
combine syntax and typing rules, such that the type of an expression tells the types
of variables that are in scope. You should implement a simple recursive function
translating types t to Set, and your interpreter should produce
values in the image of this translation.
Kilka podpowiedzi:
- Skopiować heterogeniczne listy stąd:
DepList.v -
całą sekcję hlist (ewentualnie deklaracje Implicit Arguments poniżej i notacje również)
- Parametry typu expr powinny odzwierciedlać typy zmiennych w środowisku oraz typ całego wyrażenia, dokładnie tak, jak w
Sekcji 9.2.1.
- Parametry typu pattern powinny odzwierciedlać typy zmiennych występujących w tym patternie (środowisko) oraz typ całego patternu (czyli typ wyrażenia do jakiego ten pattern możemy próbować przypasować).
- Typ konstruktora dla Case powinien uwzględniać 3 argumenty:
- wyrażenie1, które matchujemy,
- listę "par" pattern - wyrażenie,
- oraz wyrażenie2 - wartość domyślna.
Typ wszystkich patternów powinien być taki jak typ wyrażenia1, a typy wszystkich wyrażeń na liście takie jak typ wyrażenia2 - i ten sam powinien być typ całego Case'a.
Środowisko wyrażenia1 powinno być takie samo, jak środowisko wyrażenia2 oraz całego Case'a. Z kolei środowisko każdego wyrażenia na liście powinno składac się ze środowiska całego Case'a powiększonego o zmienne z odpowiedniego patternu.
Zatem "para" pattern - wyrażenie, będzie zależeć od wspólnej listy typów zmiennych - czyli będzie to faktycznie trójka, w której typ drugiego i trzeciego elementu są zależne od pierwszego. Do konstrukcji odpowiedniego typu (dla pojedynczej "pary") można uzyć typu predefiniowanego sigT2 - albo można zdefiniować sobie własną "parę" dopasowaną do naszej konkretnej sytuacji. Można też zamiast tego do kodowania całej listy par użyć typu hlist.
- Przy pisaniu interpretera głównym zadaniem będzie oczywiście interpretacja wyrażenia Case. Tam będzie występować dość zawiła rekurencja, gdyż:
- główny interpreter musi być zdefiniowany przez indukcję "po wyrażeniu"
- szukanie patternu, który dopasuje się do danego wyrażenia1 wymaga indukcji "po liście"
- sprawdzanie czy dany pattern dopasuje się faktycznie do wyrażenia1 wymaga indukcji "po patternie" - a jak się pattern dopasuje do końca, to wymaga zinterpretowania odpowiedniego wyrażenia, co zapętla rekurencję.
Żeby to ostatnie wywołanie było poprawne, musi się fizycznie znajdować wewnątrz głównego interpretera zdefiniowanego "po wyrażeniu", a zatem szukanie patternu "po liście" musi być wewnątrz rekurencji "po wyrażeniu" (tak jak to jest np. w operacji total w robionym przez nas kiedyś wspólnie ćwiczeniu o zagnieżdżonych drzewach).
Natomiast samo testowanie dopasowania konkretnego patternu może być robione w osobnej funkcji, o ile oczywiście tak to wszystko zostanie zaprojektowane, aby w przypadku sukcesu samo wywołanie interpretera nie było wewnątrz funkcji testującej.
- Ponieważ Coq trochę inaczej oblicza argumenty implicite funkcji rekurencyjnej wewnątrz jej definicji i na zewnątrz, dlatego przy pisaniu powyższego interpretera można rozważyć rezygnację z implicit arguments.