/*
In this lab, you will develop evaluation rules and typing rules for a small language.

Our language is an extended version of the one discussed in class:

e ::= true
| false
| i (Integers)
| s (Strings)
| succ e
| pred e
| iszero e
| if e then e else e
| concat e e
| isemptystr e
| strlen e

Our types must therefore include:

T ::= Bool
| Int
| String

First, write the evaluation order rules (using small-step semantics) for the expressions in the language.

Next, define the typing rules for these expressions. Be sure that your typing rules guarantee both progress and preservation. (For ways of formally guaranteeing these properties, see Chapter 8 of Ben Pierce's "Types and Programming Languages").
*/

#set page(columns: 2)

// Language keywords rendered in monospace
#let kw(body) = text(font: "DejaVu Sans Mono", size: 0.85em, body)

#let tr = kw[true]
#let fl = kw[false]
#let ife(e1, e2, e3) = [#kw[if] #e1 #kw[then] #e2 #kw[else] #e3]
#let suc(e) = [#kw[succ] #e]
#let prd(e) = [#kw[pred] #e]
#let iszero(e) = [#kw[iszero] #e]
#let concat(e1, e2) = [#kw[concat] #e1 #h(0.2em) #e2]
#let isemptystr(e) = [#kw[isemptystr] #e]
#let strlen(e) = [#kw[strlen] #e]

// Type keywords
#let bool = kw[Bool]
#let int = kw[Int]
#let string = kw[String]

// Small-step evaluation relation: e -> e'
#let sstep(e, ee) = $#e -> #ee$

// Typing relation: e : T
#let tstep(e, T) = $#e : #T$

// Rule name label in small-caps
#let rel(name) = text(size: 0.9em, smallcaps[\[#name\]])

// Rule: fraction with name on the left
// premises (content), conclusion (content)
#let rule(name, premises, conclusion) = {
  stack(
    dir: ttb,
    spacing: 0.4em,
    rel(name),
    box(stroke: 0.5pt, inset: 4pt, math.equation(
      block: true,
      numbering: none,
      math.frac(premises, conclusion),
    )),
  )
  v(0.8em)
}

= Evaluation Rules

#v(0.6em)

#rule("E-Succ-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#suc[$e$]][#suc[$e'$]]$)
#rule("E-Succ", "", $#sstep[#suc[$i$]][$i + 1$]$)

#rule("E-Pred-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#prd[$e$]][#prd[$e'$]]$)
#rule("E-Pred", "", $#sstep[#prd[$i$]][$i - 1$]$)

#rule("E-IsZero-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#iszero[$e$]][#iszero[$e'$]]$)
#rule("E-IsZero-Zero", "", $#sstep[#iszero[0]][true]$)
#rule("E-IsZero-NonZero", $i != 0$, $#sstep[#iszero[#suc[$i$]]][false]$)

#rule("E-If-Ctx", $#sstep[$e_1$][$e'_1$]$, $#sstep[#ife[$e_1$][$e_2$][$e_3$]][#ife[$e'_1$][$e_2$][$e_3$]]$)
#rule("E-If-True", "", $#sstep[#ife[true][$e_2$][$e_3$]][$e_2$]$)
#rule("E-If-False", "", $#sstep[#ife[false][$e_2$][$e_3$]][$e_3$]$)

#rule("E-Concat-Ctx1", $#sstep[$e_1$][$e'_1$]$, $#sstep[#concat[$e_1$][$e_2$]][#concat[$e'_1$][$e_2$]]$)
#rule("E-Concat-Ctx2", $#sstep[$e_2$][$e'_2$]$, $#sstep[#concat[$s_1$][$e_2$]][#concat[$s_1$][$e'_2$]]$)
#rule("E-Concat", $s_3 = s_1 + s_2$, $#sstep[#concat[$s_1$][$s_2$]][$s_3$]$)

#rule("E-IsEmptyStr-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#isemptystr[$e$]][#isemptystr[$e'$]]$)
#rule("E-IsEmptyStr-Empty", "", $#sstep[#isemptystr[`""`]][true]$)
#rule("E-IsEmptyStr-NonEmpty", [$s !=$ `""`], $#sstep[#isemptystr[$s$]][false]$)

#rule("E-StrLen-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#strlen[$e$]][#strlen[$e'$]]$)
#rule("E-StrLen-Zero", "", $#sstep[#strlen[`""`]][0]$)
#rule("E-StrLen-NonZero", [c is a single char, $s = c + s'$], $#sstep[#strlen[$s$]][#suc[#strlen[$s'$]]]$)

#pagebreak()
= Typing Rules

#v(0.6em)

#rule("T-True", "", $#tstep[true][#bool]$)
#rule("T-False", "", $#tstep[false][#bool]$)
#rule("T-Int", "", $#tstep[n][#int]$)
#rule("T-String", "", $#tstep[s][#string]$)

#rule("T-Succ", $#tstep[$e$][#int]$, $#tstep[#suc[$e$]][#int]$)
#rule("T-Pred", $#tstep[$e$][#int]$, $#tstep[#prd[$e$]][#int]$)
#rule("T-IsZero", $#tstep[$e$][#int]$, $#tstep[#iszero[$e$]][#bool]$)
#rule(
  "T-If",
  [
    $#tstep[$e_1$][#bool]$,
    $#tstep[$e_2$][$T$]$,
    $#tstep[$e_3$][$T$]$
  ],
  $#tstep[#ife[$e_1$][$e_2$][$e_3$]][T]$,
)
#rule(
  "T-Concat",
  [
    $#tstep[$e_1$][$#string$]$,
    $#tstep[$e_2$][$#string$]$
  ],
  $#tstep[#concat[$e_1$][$e_2$]][#string]$,
)
#rule(
  "T-IsEmptyStr",
  $#tstep[$e$][$#string$]$,
  $#tstep[#isemptystr[$e$]][#bool]$,
)
#rule(
  "T-StrLen",
  $#tstep[$e$][$#string$]$,
  $#tstep[#strlen[$e$]][#int]$,
)