% Version 0

\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,proof,amsthm,amssymb,color}
\usepackage{ifthen}
\usepackage{hyperref}
\newtheorem{theorem}{Theorem}
\usepackage{latexsym}
\usepackage{verbatim}
\usepackage{code,proof,amsthm,amssymb, amsmath}
\usepackage{ifthen}
\usepackage{graphics}
\usepackage{mathpartir}

% Macros that may be useful
% General stuff
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\irl}[1]{\mathtt{#1}}
\newcommand{\PFPL}{\emph{PFPL}}
\newcommand{\subst}[3]{[{#1}/{#2}]{#3}}

% Dynamic PCF Syntax (and shared syntax)
\newcommand{\ldyn}{\mathcal{L}\{\textit{dyn}\}}
\newcommand{\ok}{\irl{ok}}

\newcommand{\numc}{\irl{num}}
\newcommand{\func}{\irl{fun}}
\newcommand{\nilc}{\irl{nil}}
\newcommand{\consc}{\irl{cons}}
\newcommand{\prop}{\varphi}
\newcommand{\predopt}{\ensuremath{\prop \mathit{opt}}}

\renewcommand{\succ}[1]{\irl{succ}(#1)}
\newcommand{\z}{\irl{z}}
\newcommand{\s}[1]{\irl{s}(#1)}
\newcommand{\num}[1]{\irl{num}[#1]}
\newcommand{\numeral}[1]{\bar{#1}}
\newcommand{\ifzabs}[4]{\irl{ifz}({#1}; {#2}; {#3}.{#4})}
\newcommand{\ifz}[4]{\irl{ifz}~#1~\{\z \goesto #2~|~\s{#3}\goesto#4\}}
\newcommand{\letbinddabs}[4]{\irl{let}[{#1}]({#2},{#3}.{#4})}
\newcommand{\letbindd}[4]{\irl{let}~{#3}={#2}~\irl{in}~{#4}}
\newcommand{\letbinddr}[4]{\irl{let}~{#3} : {#1}={#2}~\irl{in}~{#4}}
\newcommand{\lamdabs}[2]{\irl{lam}({#1}. {#2})}
\newcommand{\lamd}[2]{\irl{fn}\,({#1})\,{#2}}
\newcommand{\apabs}[2]{\irl{ap}(#1; #2)}
\newcommand{\ap}[2]{#1~(#2)}
\newcommand{\fixdabs}[2]{\irl{fix}(#1.#2)}
\newcommand{\fixd}[2]{\irl{fix}~#1~\irl{is}~#2}
\newcommand{\trivabs}{\irl{triv}}
\newcommand{\triv}{\langle \rangle}
\newcommand{\pairabs}[2]{\irl{pair}({#1}; {#2})}
\newcommand{\pair}[2]{\langle {#1}, {#2} \rangle}
\newcommand{\prlabs}[1]{\irl{pr[l]}({#1})}
\newcommand{\prl}[1]{{#1}\cdot\irl{l}}
\newcommand{\prrabs}[1]{\irl{pr[r]}({#1})}
\newcommand{\prr}[1]{{#1}\cdot\irl{r}}
\newcommand{\instanceabs}[2]{\irl{instof}[{#1}]({#2})}
\newcommand{\instance}[2]{{#1}\irl{?}\,{#2}}
\newcommand{\ifnilabs}[5]{\irl{ifnil}({#1};{#2};{#3}.{#4}.{#5})}
\newcommand{\ifnil}[5]{\irl{ifnil}~{#1}~\{ \triv \goesto {#2} \mid \pair{#3}{#4} \goesto {#5} \}}
\newcommand{\condabs}[3]{\irl{cond}({#1};{#2};{#3})}
\newcommand{\cond}[3]{\irl{cond}~{#1}~{#2}~{#3}}

% Dynamic PCF judgments (and shared judgments)
\newcommand{\val}[1]{\ensuremath{{#1}~\mathsf{val}}}
\newcommand{\steps}[2]{\ensuremath{{#1} \mapsto {#2}}}
\newcommand{\err}[1]{\ensuremath{{#1}~\mathsf{err}}}
\newcommand{\isnt}[2]{\ensuremath{{#1}~\mathsf{isnt}~{#2}}}
\newcommand{\isnum}[2]{\ensuremath{{#1}~\mathsf{is\_num}~{#2}}}
\newcommand{\isfun}[3]{\ensuremath{{#1}~\mathsf{is\_fun}~{#2}.{#3}}}
\newcommand{\isnil}[1]{\ensuremath{{#1}~\mathsf{is\_nil}}}
\newcommand{\iscons}[3]{\ensuremath{{#1}~\mathsf{is\_cons}~{#2},{#3}}}

% Hybrid PCF-only syntax
\newcommand{\lhpcf}{\mathcal{L}(\mathtt{nat} \rightharpoonup \dynt)}

\newcommand{\natt}{\irl{nat}}
\newcommand{\parrtabs}[2]{\irl{parr}({#1}; {#2})}
\newcommand{\parrt}[2]{{#1} \rightharpoonup {#2}}
\newcommand{\dynt}{\irl{dyn}}
\newcommand{\unitt}{\irl{unit}}
\newcommand{\prodtabs}[2]{\irl{prod}({#1};{#2})}
\newcommand{\prodt}[2]{{#1}\times{#2}}
\newcommand{\voidt}{\irl{void}}
\newcommand{\sumtabs}[2]{\irl{sum}({#1}; {#2})}
\newcommand{\sumt}[2]{{#1} + {#2}}

\newcommand{\letbindabs}[3]{\irl{let}({#1};{#2}.{#3})}
\newcommand{\letbind}[3]{\irl{let}~{#2}={#1}~\irl{in}~{#3}}
\newcommand{\lamabs}[3]{\irl{lam}[{#1}]({#2}.{#3})}
\newcommand{\lam}[3]{\irl{fn}\,({#2}{:}{#1})\,{#3}}
\newcommand{\fix}[3]{\irl{fix}~{#2}{:}{#1}~\irl{is}~{#3}}
\newcommand{\fixabs}[3]{\irl{fix}[{#1}]({#2}.{#3})}
\newcommand{\abort}[2]{\irl{abort}[#1](#2)}
\newcommand{\inlt}[3]{\irl{inl}[#1;#2](#3)}
\newcommand{\inrt}[3]{\irl{inr}[#1;#2](#3)}
\newcommand{\inltabs}[3]{\irl{in}[#1;#2][\irl{l}](#3)}
\newcommand{\inrtabs}[3]{\irl{in}[#1;#2][\irl{r}](#3)}
\newcommand{\inl}[1]{\irl{inl}(#1)}
\newcommand{\inr}[1]{\irl{inr}(#1)}
\newcommand{\ecase}[5]{\irl{case}~{#1}~\{\inl{#2} \goesto {#3} \mid \inr{#4} \goesto {#5}\}}
\newcommand{\ecaseabs}[5]{\irl{case}({#1};{#2}.{#3};{#4}.{#5})}
\newcommand{\newabs}[2]{\irl{new}[{#1}]({#2})}
\newcommand{\new}[2]{{#1}\irl{!}\,{#2}}
\newcommand{\castabs}[2]{\irl{cast}[{#1}]({#2})}
\newcommand{\cast}[2]{{#2}\,@\,{#1}}

%% Pred

\newcommand{\nump}{\irl{num}}
\DeclareMathOperator*{\with}{\&}
\newcommand{\andpabs}[2]{\irl{and}({#1},{#2})}
\newcommand{\andp}[2]{{#1} \with {#2}}
\newcommand{\funpabs}[2]{\irl{fun}({#1},{#2})}
\newcommand{\funp}[2]{{#1} \rightharpoonup {#2}}
\newcommand{\pairpabs}[2]{\irl{pair}({#1},{#2})}
\newcommand{\pairp}[2]{{#1}\times{#2}}
\newcommand{\listp}[1]{\irl{list}({#1})}


\newcommand{\tru}{\top}
\newcommand{\subrefJ}[2]{{#1} \leq {#2}}
\newcommand{\subref}{\leq}
\newcommand{\hasRef}[2]{{#1} \in {#2}}
\newcommand{\refJ}[3]{{#1} \proves \hasRef{#2}{#3}}
\newcommand{\refJC}[2]{\refJ{\rctx}{#1}{#2}}
\newcommand{\rctx}{\Sigma}


\newcommand{\expana}[2]{#1{\ana}#2}
\newcommand{\analyze}[2]{\irl{analyze}[#2](#1)}

\newcommand{\syn}{\Rightarrow}
\newcommand{\ana}{\Leftarrow}
\newcommand{\refana}[2]{#1 \ana #2}
\newcommand{\refsyn}[2]{#1 \syn #2}
\newcommand{\anaJ}[3]{#1 \proves \refana{#2}{#3}}
\newcommand{\anaJC}[2]{\anaJ{\rctx}{#1}{#2}}
\newcommand{\synJ}[3]{#1 \proves \refsyn{#2}{#3}}
\newcommand{\synJC}[2]{\synJ{\rctx}{#1}{#2}}

\newcommand{\intro}{\text{-I}}
\newcommand{\elim}{\text{-E}}


\newcommand{\goesto}{\Rightarrow}

\newcommand{\translates}{\leadsto}
\newcommand{\transctx}[3]{{#1} \vdash {#2} \translates {#3}}
\newcommand{\trans}[2]{\transctx{\Omega}{#1}{#2}}

\newcommand{\proves}{\vdash}
\newcommand{\hasType}[2]{#1 : #2}
\newcommand{\bindType}[2]{#1{:}#2}
\newcommand{\typeJ}[3]{#1 \proves \hasType{#2}{#3}}
\newcommand{\ctx}{\Gamma}
\newcommand{\emptyCtx}{\emptyset}
\newcommand{\xCtx}[2]{\ctx, \hasType{#1}{#2}}
\newcommand{\typeJC}[2]{\typeJ{\ctx}{#1}{#2}}

\newcommand{\type}[1]{#1~\mathsf{type}}
\newcommand{\tctx}{\Delta}
\newcommand{\tformJ}[2]{#1 \vdash \type{#2}}
\newcommand{\tformJC}[1]{\tformJ{\tctx}{#1}}

\newcommand{\tlrule}{\theta\Lambda}
\newcommand{\valrule}{\textsf{v}}
\newcommand{\progrule}{\textsf{s}}
\newcommand{\elimrule}{\textsf{e}}
\newcommand{\typerule}{\textsf{t}}

\newcommand{\laz}[1]{\left[ #1 \right]}


\title{Assignment 3:
       Dynamic Typing and Refinements}
\author{15-312: Principles of Programming Languages}
\date{Name: CHANGE ME $\rightarrow$ Harry Bovik (hbovik) $\leftarrow$ CHANGE ME\\
Recitation: B}


\begin{document}
\noindent
\maketitle

\paragraph{Task 2.2 [10\%]}

\[
\inferrule{
      \trans{d}{h}
\qquad
      \trans{d_0}{h_0}
\qquad
      \transctx{\Omega,x}{d_1}{h_1}
}{ 
       \trans{\ifz{d}{d_0}{x}{d_1}}
             {\ifz{(\cast{\numc}{h})}{h_0}{y}{\subst{(\new{\numc}{y})}{x}{h_1}}}
}
\]

\paragraph{Task 2.4 [5\%]}

\[
\infer
{\trans{\ifnil{d}{d_0}{x}{y}{d_1}}
  {\ecase{(\instance{\nilc}{h})}{\_}{h_0}{\_}{h_1'}}}
{\trans{d}{h}
 &
 \trans{d_0}{h_0}
 &
 \transctx{\Omega, x, y}{d_1}{h_1}
 &
 h_1' = \subst{\prl{(\cast{\consc}{h})}{}}{x}
            {\subst{\prr{(\cast{\consc}{h})}}{y}{h_1}}}
\]

\paragraph{Task 2.5 [3\%]}

\begin{verbatim}
fix ack is fn (m) fn (n) ...
\end{verbatim}

\paragraph{Task 2.6 [2\%]}

\begin{verbatim}
fix ack ...
\end{verbatim}

\paragraph{Task 2.7 [4\%]}

\begin{verbatim}
fix ack : dyn -> dyn -> dyn is ...
\end{verbatim}

\paragraph{Task 2.8 [4\%]}

\begin{verbatim}
fix ack : nat -> nat -> nat is ...
\end{verbatim}

\paragraph{Task 2.9 [2\%]}

\begin{verbatim}
...
\end{verbatim}

\paragraph{Task 3.1 [5\%]}

\paragraph{Task 3.2 [5\%]}

\paragraph{Task 3.4 [10\%]}


\end{document}
