Compiler for LOOP language, version 1

This file defines a compiler that translates (reversibilizes) any LOOP program into a corresponding SCORE program based on a specific notion of equivalence between LOOP states and SCORE states.

Notations

• s ∼ t stands for eq_states s t (s and t are equivalent).

def Compiler.v1.l2s (P : LOOP.Com) : SCORE.Com

Syntax-directed compiler from LOOP programs to SCORE programs. The compiler takes as input a LOOP.Com and outputs the equivalent SCORE.Com.

Equations

• Compiler.v1.l2s LOOP.Com.SKIP = SCORE.Com.SKIP
• Compiler.v1.l2s (LOOP.Com.ZER x) = SCORE.Com.CON x
• Compiler.v1.l2s (LOOP.Com.ASN x y) = if x ≠ y then SCORE.Com.CON x;;SCORE.Com.FOR y (SCORE.Com.INC x) else SCORE.Com.SKIP
• Compiler.v1.l2s (LOOP.Com.INC x) = SCORE.Com.INC x
• Compiler.v1.l2s (P_2;;Q) = Compiler.v1.l2s P_2;;Compiler.v1.l2s Q
• Compiler.v1.l2s (LOOP.Com.LOOP x P_2) = SCORE.Com.FOR x (Compiler.v1.l2s P_2)

def Compiler.eq_states (s : LOOP.State) (t : SCORE.State) : Prop

Notion of equivalence between LOOP states and SCORE states. A LOOP state s is said to be equivalent to a SCORE state t if for each identifier x the value of the register identified by x in s is equal to the current value of the variable identified by x in t.

Equations

• (s∼t) = match s, t with | some σ, some τ => ∀ (x : Ident), some ↑(σ x) = (τ x).head? | x, x_1 => False

def Compiler.«term_∼_» : Lean.TrailingParserDescr

Equations

• Compiler.«term_∼_» = Lean.ParserDescr.trailingNode `Compiler.term_∼_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 51))

theorem Compiler.eq_states_update {σ : LOOP.Store} {τ : SCORE.Store} (x : Ident) (v : ℕ) : some σ∼some τ → some (σ[x ↦ v])∼some (τ[x ↦ ↑v :: τ x])

Two states are kept equivalent if the first is updated by assigning a new value v to the register identified by x and the second is updated by inserting v on top of the stack identified by x.

theorem Compiler.v1.soundness {s : LOOP.State} {t : SCORE.State} (P : LOOP.Com) : s∼t → LOOP.eval P s∼SCORE.eval (Compiler.v1.l2s P) t

Let P be a LOOP program, σ a LOOP state and τ a SCORE state. If the two states are equivalent, then the evaluation of P in σ and the compiled SCORE program l2s P in τ end in two equivalent states.