Domácí úkoly 3:

V následujících úkolech bude využita níže uvedená implementace aritmetických výrazů. Jak vidíte, ve výrazech se mohou vyskytovat proměnné. Tyto proměnné jsou reprezentovány datovým typem var, který je zde implementován pomocí datového typu string. Typ state reprezentuje aktuální přiřazení hodnot proměnným. Pro jednoduchost jsou proměnným přiřazovány pouze hodnoty typu nat.

Definice aritmetických výrazů:

Definice koercí a uživatelsky definovaných notací pro usnadnění zápisu aritmetických výrazů:

Funkce pro vyhodnocení hodnoty aritmetického výrazu:

Příklad A: 1 bod

Staré kalkulačky HP, programovací jazyky jako Forth a Postscript i abstraktní stroje jako Java Virtual Machine všechny vyhodnocují aritmetické výrazy pomocí zásobníku. Například výraz

       (2*3)+(3*(4-2))

by byl zapsán jako

       2 3 * 3 4 2 - * +

a vyhodnocen následujícím způsobem (kde program, který je vyhodnocován, je zobrazen vpravo a obsah zásobníku vlevo):

      [ ]           |    2 3 * 3 4 2 - * +
      [2]           |    3 * 3 4 2 - * +
      [3, 2]        |    * 3 4 2 - * +
      [6]           |    3 4 2 - * +
      [3, 6]        |    4 2 - * +
      [4, 3, 6]     |    2 - * +
      [2, 4, 3, 6]  |    - * +
      [2, 3, 6]     |    * +
      [6, 6]        |    +
      [12]          |

Cílem tohoto cvičení je napsat malý kompilátor, který přeloží výrazy typu aexp na instrukce zásobníkového stroje. Instrukční sada našeho zásobníkového stroje se bude skládat z následujících instrukcí:

• SPush n: Uloží číslo n na zásobník.
• SLoad x: Načte hodnotu proměnné x z aktuálního stavu a uloží ji na zásobník.
• SPlus: Odebere z vrcholu zásobníku dvě čísla, sečte je a výsledek uloží na zásobník.
• SMinus: Podobné, ale odečte první číslo od druhého.
• SMult: Podobné, ale čísla vynásobí.

Napište funkci, která vyhodnotí programy ve výše popsaném zásobníkovém jazyce. Tato funkce dostane jako vstup aktuální stav přiřazující hodnoty proměnným, počáteční obsah zásobníku, který je reprezentován jako seznam tvořený čísly (vrchol zásobníku odpovídá začátku seznamu), a program reprezentovaný jako seznam tvořený jednotlivými instrukcemi. Funkce by měla vrátit jako výsledek seznam reprezentující obsah zásobníku po vykonání daného programu. Otestujte vaši funkci na níže uvedených příkladech. Všimněte si, že není specifikováno, co se má udělat v případě, kdy se má provést instrukce SPlus, SMinus nebo SMult a zásobník obsahuje méně než dva prvky. Z určitého pohledu se dá říci, že na tom nezáleží, protože korektní kompilátor nikdy nevyprodukuje takový chybně utvořený program. Pro jednoduchost bude asi nejsnadnější takovou problematickou instrukci přeskočit a pokračovat vykonáváním následujících instrukcí.

☐

Příklad B: 1 bod

Dále napište funkci, která zkompiluje výraz typu aexp do podoby programu pro zásobníkový stroj. Výsledek provedení daného programu by měl být stejný jako uložit hodnotu daného výrazu na vrchol zásobníku pomocí instrukce push.

Poté, co definujete funkci s_compile, dokažte následující tvrzení, abyste ověřili, že vaše funkce funguje správně.

☐

Příklad C: 1 bod

Vykonávání instrukcí zásobníkového stroje je možné v následujícím smyslu rozložit: vykonat zásobníkový program p1 ++ p2 je to samé jako vykonat instrukce p1, vzít výsledný obsah zásobníku a vykonat instrukce p2 s tímto obsahem zásobníku jako s počátečním stavem. Dokažte, že to tak opravdu je.

☐

Příklad D: 2 body

Nyní dokažte korektnost kompilátoru navrženého v příkladu B. Začněte tím, že dokážete následující lemma. Pokud se ukáže, že je to příliš složité, zvažte, zda není možné nějak zjednodušit vaši implementaci funkcí s_execute a s_compile.

Hlavní teorém by pak měl být velmi snadno odvoditelným důsledkem výše uvedeného lemmatu.

☐