(*----------------------------------------------------------------------------*) From Stdlib Require Import Lists.List. Import ListNotations. From Stdlib Require Import Strings.String. (** 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]. *) Definition var := string. Definition var_eqb : var -> var -> bool := String.eqb. Definition state := var -> nat. Definition empty_st (_ : var) := 0. Definition update_state (st : state) (x : var) (v : nat) := fun x' => if var_eqb x x' then v else st x'. Notation "x '!->' v ';' st" := (update_state st x v) (at level 100, v at next level, right associativity). Notation "x '!->' v" := (x !-> v ; empty_st) (at level 100). (** Definice aritmetických výrazů: *) Inductive aexp : Type := | ANum (n : nat) | AId (x : var) | APlus (a1 a2 : aexp) | AMinus (a1 a2 : aexp) | AMult (a1 a2 : aexp). Definition X : var := "X"%string. Definition Y : var := "Y"%string. (** Definice koercí a uživatelsky definovaných notací pro usnadnění zápisu aritmetických výrazů: *) Coercion AId : var >-> aexp. Coercion ANum : nat >-> aexp. Declare Custom Entry com. Declare Scope com_scope. Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope. Notation "( x )" := x (in custom com, x at level 99) : com_scope. Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope. Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity). Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity). Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity). Open Scope com_scope. (** Funkce pro vyhodnocení hodnoty aritmetického výrazu: *) Fixpoint aeval (st : state) (a : aexp) : nat := match a with | ANum n => n | AId x => st x | <{a1 + a2}> => (aeval st a1) + (aeval st a2) | <{a1 - a2}> => (aeval st a1) - (aeval st a2) | <{a1 * a2}> => (aeval st a1) * (aeval st a2) end. (*----------------------------------------------------------------------------*) (** **** 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í. *) Inductive sinstr : Type := | SPush (n : nat) | SLoad (x : var) | SPlus | SMinus | SMult. (** 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í. *) Fixpoint s_execute (st : state) (stack : list nat) (prog : list sinstr) : list nat (* NAHRAĎTE TENTO ŘÁDEK ":= _vaše_definice ." *). Admitted. Check s_execute. Example s_execute1 : s_execute empty_st [] [SPush 5; SPush 3; SPush 1; SMinus] = [2; 5]. (* ZDE DOPLŇTE DŮKAZ *) Admitted. Example s_execute2 : s_execute (X !-> 3) [3;4] [SPush 4; SLoad X; SMult; SPlus] = [15; 4]. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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. *) Fixpoint s_compile (e : aexp) : list sinstr (* NAHRAĎTE TENTO ŘÁDEK ":= _vaše_definice ." *). Admitted. (** Poté, co definujete funkci [s_compile], dokažte následující tvrzení, abyste ověřili, že vaše funkce funguje správně. *) Example s_compile1 : s_compile <{ X - (2 * Y) }> = [SLoad X; SPush 2; SLoad Y; SMult; SMinus]. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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. *) Theorem execute_app : forall st p1 p2 stack, s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*) (** **** 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]. *) Lemma s_compile_correct_aux : forall st e stack, s_execute st stack (s_compile e) = aeval st e :: stack. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** Hlavní teorém by pak měl být velmi snadno odvoditelným důsledkem výše uvedeného lemmatu. *) Theorem s_compile_correct : forall (st : state) (e : aexp), s_execute st [] (s_compile e) = [ aeval st e ]. Proof. (* ZDE DOPLŇTE DŮKAZ *) Admitted. (** [] *) (*----------------------------------------------------------------------------*)