\begin{code}\>\<%
\\
\>\AgdaKeyword{module} \AgdaModule{Source} \AgdaKeyword{where}\<%
\\
%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Data.Bool} \AgdaKeyword{using} \AgdaSymbol{(}if\_then\_else\_\AgdaSymbol{)} \AgdaKeyword{renaming} \AgdaSymbol{(}Bool \AgdaSymbol{to} 𝔹\AgdaSymbol{)}\<%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Data.Vec} \AgdaKeyword{using} \AgdaSymbol{(}Vec\AgdaSymbol{;} [\_]\AgdaSymbol{;} head\AgdaSymbol{)} \AgdaKeyword{renaming} \AgdaSymbol{(}\_++\_ \AgdaSymbol{to} \_+++\_\AgdaSymbol{)}\<%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Data.Nat} \AgdaKeyword{using} \AgdaSymbol{(}ℕ\AgdaSymbol{;} \_+\_\AgdaSymbol{;} suc\AgdaSymbol{)}\<%
\\
\>\<\end{code}

First of all, as our expression language is typed, we need a language of types
We denote the types of the Src language with similar symbols of the
corresponding types in Agda, subscripted with a lower-case "s"

%<*tys>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{Tyₛ} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{ℕₛ} \AgdaSymbol{:} \AgdaDatatype{Tyₛ}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{𝔹ₛ} \AgdaSymbol{:} \AgdaDatatype{Tyₛ}\<%
\\
\>\<\end{code}
%</tys>

Together with defining the object language types,
we define a mapping from object language types into Agda types.

\begin{code}\>\<%
\\
\>\AgdaFunction{⁅\_⁆} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{α} \AgdaSymbol{:} \AgdaDatatype{Tyₛ}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\<%
\\
\>\AgdaFunction{⁅} \AgdaInductiveConstructor{ℕₛ} \AgdaFunction{⁆} \AgdaSymbol{=} \AgdaDatatype{ℕ}\<%
\\
\>\AgdaFunction{⁅} \AgdaInductiveConstructor{𝔹ₛ} \AgdaFunction{⁆} \AgdaSymbol{=} \AgdaDatatype{𝔹}\<%
\\
\>\<\end{code}

Now we can define an inductive family for the expressions of our object language,
indexed by their src language type (Tyₛ). We also use subscripted notation
to avoid confusion with Agda's standard library symbols.

\begin{code}\>\<%
\\
\>\AgdaFunction{Sizeₛ} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\<%
\\
\>\AgdaFunction{Sizeₛ} \AgdaSymbol{=} \AgdaDatatype{ℕ}\<%
\\
\>\<\end{code}

%<*src>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{Src} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{t} \AgdaSymbol{:} \AgdaDatatype{Tyₛ}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{z} \AgdaSymbol{:} \AgdaFunction{Sizeₛ}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{vₛ} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{v} \AgdaSymbol{:} \AgdaFunction{⁅} \AgdaBound{t} \AgdaFunction{⁆}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaNumber{1}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{\_+ₛ\_} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{e₁} \AgdaBound{e₂} \AgdaSymbol{:} \AgdaDatatype{Src} \AgdaInductiveConstructor{ℕₛ} \AgdaNumber{1}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaInductiveConstructor{ℕₛ} \AgdaNumber{1}\<%
\\
\>\<\end{code}
%</src>
\begin{code}\>\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{ifₛ\_thenₛ\_elseₛ\_} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t} \AgdaBound{n}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{c} \AgdaSymbol{:} \AgdaDatatype{Src} \AgdaInductiveConstructor{𝔹ₛ} \AgdaNumber{1}\AgdaSymbol{)}\<%
\\
\>[4]\AgdaIndent{24}{}\<[24]%
\>[24]\AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{eₜ} \AgdaBound{eₑ} \AgdaSymbol{:} \AgdaDatatype{Src} \AgdaBound{t} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{n}\AgdaSymbol{))} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{n}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{\_⟫ₛ\_} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t} \AgdaBound{m} \AgdaBound{n}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{n}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{n} \AgdaPrimitive{+} \AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaKeyword{infixl} \AgdaNumber{40} \_+ₛ\_\<%
\\
\>\<\end{code}


The evaluation function defined below is a denotational semantics for the src language.
Evaluation takes a typed expression in our src language_ to a typed Agda value.
We denote evaluation by using the usual "semantic brackets", "⟦" and "⟧".

\begin{code}\>\<%
\\
\>\AgdaKeyword{mutual}\<%
\\
\>\<\end{code}
%<*eval>
\begin{code}\>\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦\_⟧} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{t} \AgdaSymbol{:} \AgdaDatatype{Tyₛ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{z} \AgdaSymbol{:} \AgdaFunction{Sizeₛ}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{e} \AgdaSymbol{:} \AgdaDatatype{Src} \AgdaBound{t} \AgdaBound{z}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Vec} \AgdaFunction{⁅} \AgdaBound{t} \AgdaFunction{⁆} \AgdaBound{z}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦} \AgdaInductiveConstructor{vₛ} \AgdaBound{v} \AgdaFunction{⟧} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaFunction{[} \AgdaBound{v} \AgdaFunction{]}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦} \AgdaBound{e₁} \AgdaInductiveConstructor{+ₛ} \AgdaBound{e₂} \AgdaFunction{⟧} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaFunction{[} \AgdaFunction{⟦} \AgdaBound{e₁} \AgdaFunction{⟧'} \AgdaPrimitive{+} \AgdaFunction{⟦} \AgdaBound{e₂} \AgdaFunction{⟧'} \AgdaFunction{]} \<[57]%
\>[57]\<%
\\
\>\<\end{code}
%</eval>
\begin{code}\>\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦} \AgdaInductiveConstructor{ifₛ\_thenₛ\_elseₛ\_} \AgdaBound{c} \AgdaBound{e₁} \AgdaBound{e₂} \AgdaFunction{⟧} \AgdaSymbol{=} \AgdaFunction{if} \AgdaFunction{⟦} \AgdaBound{c} \AgdaFunction{⟧'} \AgdaFunction{then} \AgdaFunction{⟦} \AgdaBound{e₁} \AgdaFunction{⟧} \AgdaFunction{else} \AgdaFunction{⟦} \AgdaBound{e₂} \AgdaFunction{⟧}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦} \AgdaBound{e₁} \AgdaInductiveConstructor{⟫ₛ} \AgdaBound{e₂} \AgdaFunction{⟧} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaFunction{⟦} \AgdaBound{e₂} \AgdaFunction{⟧} \AgdaFunction{+++} \AgdaFunction{⟦} \AgdaBound{e₁} \AgdaFunction{⟧}\<%
\\
%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦\_⟧'} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{σ} \AgdaSymbol{:} \AgdaDatatype{Tyₛ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{z'} \AgdaSymbol{:} \AgdaFunction{Sizeₛ}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{e} \AgdaSymbol{:} \AgdaDatatype{Src} \AgdaBound{σ} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{z'}\AgdaSymbol{))} \AgdaSymbol{→} \AgdaFunction{⁅} \AgdaBound{σ} \AgdaFunction{⁆}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaFunction{⟦} \AgdaBound{e} \AgdaFunction{⟧'} \AgdaSymbol{=} \AgdaFunction{head} \AgdaFunction{⟦} \AgdaBound{e} \AgdaFunction{⟧}\<%
\\
\>\<\end{code}
