CaZzzer/cs-252
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

lab14: impl typing rules

Browse Source
This commit is contained in:
Yura
2026-04-14 15:41:29 -07:00
parent 4a784531c2
commit 9374144565
2 changed files with 1472 additions and 699 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2085
lab14/typed-semantics.pdf
View File

File diff suppressed because it is too large Load Diff

86
lab14/typed-semantics.typ
View File

@@ -39,15 +39,23 @@ Next, define the typing rules for these expressions. Be sure that your typing ru
#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\]])
// Small-step rule: fraction with name on the left
// Rule: fraction with name on the left
// premises (content), conclusion (content)
#let ssrule(name, premises, conclusion) = {
#let rule(name, premises, conclusion) = {
grid(
columns: (auto, auto),
column-gutter: 1em,
@@ -68,32 +76,68 @@ Next, define the typing rules for these expressions. Be sure that your typing ru
#v(0.6em)
#ssrule("E-Succ-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#suc[$e$]][#suc[$e'$]]$)
#ssrule("E-Succ", "", $#sstep[#suc[$i$]][$i + 1$]$)
#rule("E-Succ-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#suc[$e$]][#suc[$e'$]]$)
#rule("E-Succ", "", $#sstep[#suc[$i$]][$i + 1$]$)
#ssrule("E-Pred-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#prd[$e$]][#prd[$e'$]]$)
#ssrule("E-Pred", "", $#sstep[#prd[$i$]][$i - 1$]$)
#rule("E-Pred-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#prd[$e$]][#prd[$e'$]]$)
#rule("E-Pred", "", $#sstep[#prd[$i$]][$i - 1$]$)
#ssrule("E-IsZero-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#iszero[$e$]][#iszero[$e'$]]$)
#ssrule("E-IsZero-Zero", "", $#sstep[#iszero[0]][true]$)
#ssrule("E-IsZero-NonZero", $i != 0$, $#sstep[#iszero[#suc[$i$]]][false]$)
#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]$)
#ssrule("E-If-Ctx", $#sstep[$e_1$][$e'_1$]$, $#sstep[#ife[$e_1$][$e_2$][$e_3$]][#ife[$e'_1$][$e_2$][$e_3$]]$)
#ssrule("E-If-True", "", $#sstep[#ife[true][$e_2$][$e_3$]][$e_2$]$)
#ssrule("E-If-False", "", $#sstep[#ife[false][$e_2$][$e_3$]][$e_3$]$)
#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$]$)
#ssrule("E-Concat-Ctx1", $#sstep[$e_1$][$e'_1$]$, $#sstep[#concat[$e_1$][$e_2$]][#concat[$e'_1$][$e_2$]]$)
#ssrule("E-Concat-Ctx2", $#sstep[$e_2$][$e'_2$]$, $#sstep[#concat[$s_1$][$e_2$]][#concat[$s_1$][$e'_2$]]$)
#ssrule("E-Concat", $s_3 = s_1 + s_2$, $#sstep[#concat[$s_1$][$s_2$]][$s_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$]$)
#ssrule("E-IsEmptyStr-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#isemptystr[$e$]][#isemptystr[$e'$]]$)
#ssrule("E-IsEmptyStr-Empty", "", $#sstep[#isemptystr[`""`]][true]$)
#ssrule("E-IsEmptyStr-NonEmpty", [$s !=$ `""`], $#sstep[#isemptystr[$s$]][false]$)
#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]$)
#ssrule("E-StrLen-Ctx", $#sstep[$e$][$e'$]$, $#sstep[#strlen[$e$]][#strlen[$e'$]]$)
#ssrule("E-StrLen-Zero", "", $#sstep[#strlen[`""`]][0]$)
#ssrule("E-StrLen-NonZero", [c is a single char, $s = c + s'$], $#sstep[#strlen[$s$]][#suc[#strlen[$s'$]]]$)
#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'$]]]$)
== 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]$,
)