PLT Exam of Jan 2020, solution transcript of 2021-12-16 # Q3 Seq. S ::= P M ; Plus. P ::= P A "+"; None. P ::= ; Minus. M ::= A "-" M ; Done. M ::= A ; X. A ::= "x" ; Y. A ::= "y" ; . x + y - x -- reduce None P . x + y - x -- shift x P x . + y - x -- reduce X P A . + y - x -- shift + P A + . y - x -- reduce Plus P . y - x -- shift y P y . - x -- reduce Y P A . - x -- shift - P A - . x -- shift x P A - x . -- reduce X P A - A . -- reduce Done P A - M . -- reduce Minus P M . -- reduce Seq S -- accept # Q4 ## Type checking Judgement Γ ⊢ s ⇒ Γ' Contexts Γ are .-separated lists of finite maps Δ from identifiers x to types t. - Blocks Γ ⊢ b ⇒ Γ' Γ.ε ⊢ ss ⇒ Γ' ------------------------ Γ ⊢ { ss } ⇒ Γ - Statement sequences Γ ⊢ ss ⇒ Γ' --------- Γ ⊢ ε ⇒ Γ Γ ⊢ s ⇒ Γ₁ Γ₁ ⊢ ss ⇒ Γ₂ --------------------------- Γ ⊢ s ss ⇒ Γ₂ - Statements Γ ⊢ s ⇒ Γ' Initialization "t x; x = e;" Γ.(Δ,x:t) ⊢ e : t ----------------------------- x ∉ Δ Γ.Δ ⊢ (t x = e;) ⇒ Γ.(Δ,x:t) Expression as statement Γ ⊢ e : t ----------- Γ ⊢ e; ⇒ Γ If-else Γ ⊢ e : bool Γ.ε ⊢ s₁ ⇒ _ Γ.ε ⊢ s₂ ⇒ _ ---------------------------------------------- Γ ⊢ if (e) s₁ else s₂ ⇒ Γ ### Alternative for type checker: only return addition to context Judgement Γ ⊢ s ⇒ Δ Contexts Γ are .-separated lists of finite maps Δ from identifiers x to types t. - Blocks Γ ⊢ b Γ.ε ⊢ ss ------------ Γ ⊢ { ss } - Statement sequences Γ ⊢ ss ----- Γ ⊢ ε Γ.Δ ⊢ s ⇒ Δ' Γ.(Δ,Δ') ⊢ ss ------------------------------- Γ.Δ ⊢ s ss - Statements Γ ⊢ s ⇒ Δ Initialization "t x; x = e;" Γ.(Δ,x:t) ⊢ e : t ----------------------------- x ∉ Δ Γ.Δ ⊢ (t x = e;) ⇒ (x:t) Expression as statement Γ ⊢ e : t ----------- Γ ⊢ e; ⇒ () If-else Γ ⊢ e : bool Γ.ε ⊢ s₁ ⇒ _ Γ.ε ⊢ s₂ ⇒ _ ---------------------------------------------- Γ ⊢ if (e) s₁ else s₂ ⇒ () ## Interpretation of expressions Judgement: γ ⊢ e ⇒ ⟨v; γ'⟩ An environment γ is a finite map from identifiers x to values v. A value is an integer or boolean literal. Expressions: – boolean literal true or false γ ⊢ true ⇒ ⟨ true; γ ⟩ γ ⊢ false ⇒ ⟨ false; γ ⟩ – integer literal γ ⊢ i ⇒ ⟨ i; γ ⟩ – function call with a list of comma-separated arguments Function: t f (t₁ x₁, ... tₙ xₙ) b γ ⊢ e₁ ⇒ ⟨ v₁; γ₁ ⟩ γ₁ ⊢ e₂ ⇒ ⟨ v₂; γ₂ ⟩ ... γₙ-₁ ⊢ eₙ ⇒ ⟨ vₙ; γₙ ⟩ x₁=v₁,...,xₙ=vₙ ⊢ b ⇒ v ---------------------------- γ ⊢ f(e₁,...,eₙ) ⇒ ⟨ v; γₙ ⟩ – post-increment of an identifier, e.g., x++ -------------------------- γ(x)=i γ ⊢ x++ ⇒ ⟨ i; γ[x=i+1] ⟩ – addition (+), left associative γ ⊢ e₁ ⇒ ⟨ i₁; γ₁ ⟩ γ₁ ⊢ e₂ ⇒ ⟨ i₂; γ₂ ⟩ ----------------------------- γ ⊢ e₁ + e₂ ⇒ ⟨ i₁ + i₂; γ₂ ⟩ # Q5 Compilation ## Compilation schemes • Block: a sequence of statements enclosed between { and } compile( { ss } ): newBlock for (s : ss) compile (s) popBlock • Statement: – block – initializing variable declaration, e.g., int x = e; compile ( t x = e; ): a <- addVar t x compile (e) emit (istore a) – statement formed from an expression by adding a semicolon ; compile ( e; ): compile (e) emit (pop) – if statement with else compile ( if e s₁ else s₂ ): Lfalse,Lend <- newLabel compile(e) emit (ifeq Lfalse) compile (s₁) emit (goto Lend) emit (Lfalse:) compile (s₂) emit (Lend:) • Expression: – boolean literal true or false compile (true): emit (ldc 1) compile (false): emit (ldc 0) – integer literal compile (i): emit (ldc i) – function call with a list of comma-separated arguments compile ( f(es) ) fname ← lookupFun f for (e : es) compile(e) emit (invokestatic fname) – post-increment of an identifier, e.g., x++ compile ( x++ ): a ← lookupVar x emit (iload a) emit (dup) emit (ldc 1) emit (iadd) emit (istore a) – addition (+), left associative compile ( e₁ + e₂ ): compile (e₁) compile (e₂) emit (iadd) ## Small-step semantics c : (P,V,S) → (P',V',S') istore a: (P, V, S.i) → (P+1, V[a=i], S) iload a : (P, V, S) → (P+1, V, S.V[a]) pop : (P, V, S.i) → (P+1, V, S) dup : (P, V, S.i) → (P+1, V, S.i.i) ldc i : (P, V, S) → (P+1, V, S.i) iadd : (P, V, S.i.j) → (P+1, V, S.(i+j)) goto l : (P, V, S) → (l, V, S) ifeq l : (P, V, S.0) → (l, V, S) ifeq l : (P, V, S.i) → (P+1, V, S) if i ≠ 0 invokestatic f : (P, V, S.v₁...vₙ) → (P+1, V, S.v) if f(v₁,...,vₙ)=v # Q6 Call-by-name interpreter Judgement: γ ⊢ e ⇒ v Environments γ,δ are finite maps from identifiers x to closures ⟨ e; δ ⟩. Values v are integer literals i or function closures ⟨ λx→e; δ ⟩. δ ⊢ e ⇒ v ---------- γ(x) = ⟨ e; δ ⟩ γ ⊢ x ⇒ v ---------------------- γ ⊢ λx→e ⇒ ⟨ λx→e; γ ⟩ --------------- γ ⊢ i ⇒ i γ ⊢ e₁ ⇒ i₁ γ ⊢ e₂ ⇒ i₂ --------------------- γ ⊢ e₁ + e₂ ⇒ i₁ + i₂ γ ⊢ f ⇒ ⟨ λx→e'; δ ⟩ δ,x=⟨e;γ⟩ ⊢ e' ⇒ v ------------------------ γ ⊢ f e ⇒ v