diff --git a/doc/bool.ott b/doc/bool.ott index 46d4a4b..e845e93 100644 --- a/doc/bool.ott +++ b/doc/bool.ott @@ -15,27 +15,33 @@ v :: 'v_' ::= | Bool :: :: TyBool | True :: :: LitTrue | False :: :: LitFalse - | if ne then a else b :: :: If neutral , ne :: 'n_' ::= | if ne then a else b :: :: If +nf :: 'nf_' ::= + | Bool :: :: TyBool + | True :: :: LitTrue + | False :: :: LitFalse + | if ne then a else b :: :: If + + defns Jwhnf :: '' ::= defn -whnf a ~> v :: :: whnf :: 'whnf_' +whnf a ~> nf :: :: whnf :: 'whnf_' by whnf a ~> True -whnf b1 ~> v +whnf b1 ~> nf --------------------------- :: if_true -whnf if a then b1 else b2 ~> v +whnf if a then b1 else b2 ~> nf whnf a ~> False -whnf b2 ~> v +whnf b2 ~> nf ------------------------------- :: if_false -whnf if a then b1 else b2 ~> v +whnf if a then b1 else b2 ~> nf ----------------- :: bool whnf Bool ~> Bool diff --git a/doc/data.ott b/doc/data.ott index f631610..5b57372 100644 --- a/doc/data.ott +++ b/doc/data.ott @@ -29,11 +29,15 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }} v :: 'v_' ::= | K args :: :: TCon | T args :: :: DCon - | case ne of { ai // i /> } :: :: Case neutral, ne :: 'n_' ::= | case ne of { ai // i /> } :: :: Case +nf :: 'nf_' ::= + | K args :: :: TCon + | T args :: :: DCon + | case ne of { ai // i /> } :: :: Case + args {{ tex \overline{a} }} , bs {{ tex \overline{b} }} :: '' ::= | :: :: Nil @@ -78,7 +82,7 @@ defns Jwhnf :: '' ::= defn -whnf a ~> v :: :: whnf :: 'whnf_' +whnf a ~> nf :: :: whnf :: 'whnf_' by -------------------- :: tcon @@ -88,9 +92,9 @@ whnf T args ~> T args whnf K args ~> K args match (K args) (pati -> ai) ~> b -whnf b ~> v +whnf b ~> nf ---------------------------------------------------------------------- :: case -whnf case (K args) of { ai // i /> } ~> v +whnf case (K args) of { ai // i /> } ~> nf a ~> ne ------------------------------------------------------------------------------- :: case_cong diff --git a/doc/epsilon.ott b/doc/epsilon.ott index b55197d..2ecfc00 100644 --- a/doc/epsilon.ott +++ b/doc/epsilon.ott @@ -43,7 +43,7 @@ defns Jwhnf :: '' ::= defn -whnf a ~> v :: :: whnf :: 'whnf_' +whnf a ~> nf :: :: whnf :: 'whnf_' by defns diff --git a/doc/oplss.mng b/doc/oplss.mng index 2ba9fd1..5c333e6 100644 --- a/doc/oplss.mng +++ b/doc/oplss.mng @@ -1251,7 +1251,8 @@ The main idea is that we will: \item Figure out how to revise the \emph{algorithmic} version of our type - system so that it supports the above rule. + system so that it supports the above rule, deferring to an algorithmic + version of equality. \end{itemize} What is a good definition of equality? We have implicitly started with a very @@ -1333,6 +1334,8 @@ $\Pi$-type, then we can access its subcomponents. has already been reduced to normal form. This will allow \rref{c-lambda} to match against a literal function type. +\[ \drule[width=4in]{c-whnf} \] + \end{itemize} \begin{figure} @@ -1345,19 +1348,20 @@ match against a literal function type. The following judgment (shown in Figure~\ref{fig:whnf}) % -\[ \fbox{$[[whnf a ~> v]]$} \] +\[ \fbox{$[[whnf a ~> nf]]$} \] % -describes when a term $[[a]]$ reduces to some result $[[v]]$ in \emph{weak +describes when a term $[[a]]$ reduces to some result $[[nf]]$ in \emph{weak head normal form (whnf)}. For closed terms, these rules correspond to a big-step evaluation relation and produce a value (i.e. abstraction or type -form). For open terms, the rules could also produce terms that are some +form). For open terms, the rules could also produce terms that are a sequence of applications headed by a variable. In this case, we call the term a \emph{neutral} term, and use the metavariable $[[ne]]$ to refer to it. \[ \begin{array}{llcl} -\textit{value} & [[v]] & ::= & [[Type]]\ |\ [[\x.a]]\ |\ [[(x:A) -> B]]\ |\ [[()]]\ |\ [[Unit]]\ |\ [[ne]] \\ +\textit{value} & [[v]] & ::= & [[\x.a]]\ [[Type]]\ |\ [[(x:A) -> B]]\ \\ \textit{neutral terms} & [[ne]] & ::= & [[x]]\ |\ [[ne a]] \\ +\textit{weak-head normal form} & [[nf]] & ::= & [[v]]\ |\ [[ne]] \\ \end{array} \] @@ -1429,11 +1433,17 @@ of \texttt{inferType} \subsection{Implementing definitional equality (see Equal.hs)} \label{sec:equate} +\begin{figure} +\drules[eq]{$[[G |- A <=> B]]$}{Algorithmic equality}{refl,whnf,abs,pi,app} +\caption{Algorithmic equality for core \pif} +\label{fig:algeq} +\end{figure} + + The rules for $[[G |- a = b ]]$ \emph{specify} when terms should be equal, but they are not an algorithm. But how do we implement its algorithmic analogue $[[G |- a <=> b]]$? - There are several ways to do so. The easiest one to explain is based on reduction---for \texttt{equate} to @@ -1450,8 +1460,11 @@ One way to do this is with the following algorithm: \end{verbatim} However, we can do better. Sometimes we can find out that terms are -equivalent without fully reducing them. Because reduction can be expensive (or -even nonterminating) we would like to only reduce as much as necessary. +equivalent without fully reducing them. For example, if we observe that the +two terms are already $\alpha$-equavalent, then we already know that they are +equal---no need to reduce them first. Because reduction can be expensive (or +even nonterminating) we would like to only reduce as much as we need to find +out whether the terms can be identified. Therefore, the implementation of \cd{equate} has the following form. \begin{verbatim} @@ -1474,8 +1487,8 @@ Therefore, the implementation of \cd{equate} has the following form. -- | head forms don't match throw an error (_,_) -> Env.err ... \end{verbatim} -Above, we first check whether the terms are already alpha-equivalent. If they -are, we do not need to do anything else, we can return immediately +Above, we first check for alpha-equivalence. If they +are, we do not need to do anything else. Instead, the function returns immediately (i.e., without throwing an error, which is what the function does when it decides that the terms are not equal). The next step is to reduce both terms to their weak head normal forms. If two terms have different head forms, then @@ -1483,26 +1496,30 @@ we know that they must be different terms, so we can throw an error. If they hav the same head forms, then we can call the function recursively on analogous subcomponents until the function either terminates or finds a mismatch. +This algorithm is summarized in Figure~\ref{fig:algeq}. + Why do we use weak head reduction vs.~full reduction? \begin{itemize} -\item - We can implement deferred substitutions for variables. Note that when - comparing terms we need to have their definitions available. That way we - can compute that \texttt{(plus\ 3\ 1)} weak head normalizes to 4, by - looking up the definition of \texttt{plus} when needed. However, we - don't want to substitute all variables through eagerly---not only does - this make extra work, but error messages can be extremely long. +\item We can extend this algorithm to implement deferred substitutions for + variables. Note that when comparing terms we need to have their definitions + available. That way we can compute that \texttt{(plus\ 3\ 1)} weak head + normalizes to 4, by looking up the definition of \texttt{plus} when + needed. However, we don't want to substitute all variables through + eagerly---not only does this make extra work, but error messages can be + extremely long. \item Furthermore, we allow recursive definitions in \pif, so normalization may just fail completely if we unfold recursive definitions inside functions before they are applied. In contrast, the definition based on \texttt{whnf} only unfolds recursive definitions when they stand in the way of equivalence, so avoids some infinite loops in the type checker. - - Note that we don't have a complete treatment of equality. There will always - be terms that can cause \texttt{equate} to loop forever. \end{itemize} +Note that equality is not decidable in \texttt{pi-forall}. There will always +be terms that could cause \texttt{equate} to loop forever. However, the +algorithm is sound. If it says that two terms are equal, then there is some +derivation using the rules of Figure~\ref{fig:defeq} that the terms are equal. + \section{Dependent pattern matching and propositional equality} \label{sec:pattern-matching} @@ -1755,9 +1772,13 @@ with an equivalent type. \[ \drule[width=4in]{t-subst-simple} \] -How can we implement this rule? For simplicity, we will play the same trick that -we did with booleans, requiring that one of the sides of the equality be a -variable. +How can we implement this rule? For simplicity in these lecture notes, we will +play the same trick that we did with booleans, requiring that one of the sides +of the equality be a variable.\footnote{The \pif implementation implements a more +expressive rule that uses \emph{unification} to determine the substitution to apply +to $A$. Unification means that if we have an equality type such as +$[[(x, True) = ( (), y)]]$ +then we can produce the substitution of $[[()]]$ for $[[x]]$ and $[[True]]$ for $[[y]]$.} \[ \drule[width=4in]{c-subst-left-simple} \] \[ \drule[width=4in]{c-subst-right-simple} \] @@ -1885,21 +1906,22 @@ evaluate to \texttt{Refl} we could erase it. We need to make sure that an irrelevant variable is not ``used'' in the relevant parts of the body of a $\lambda$-abstraction. How can we do so? -The key idea is that we mark variables in the context with an $[[ep]]$ -annotation, which is either $[[Rel]]$ (relevant) or $[[Irr]]$ (irrelevant). -``Normal'' variables, introduced by $\lambda$-expressions, will always be -marked as relevant, and only relevant variables can be used in terms. As a -result, we revise the variable typing rule to require the relevant annotation. -In the \texttt{version3} implementation, type signatures in the environment now -include an \cd{Epsilon} tag, and the function \cd{checkStage} ensures that this -tag is $[[Rel]]$ when the variable is used in the term. +The key idea is that we mark variable assumptions in the context with an +$\epsilon$ annotation, which is either $[[Rel]]$ (relevant) or $[[Irr]]$ +(irrelevant). and only relevant variables can be used in terms. (``Normal'' +variables, introduced by $\lambda$-expressions, will always be marked as +relevant.) As a result, we revise the variable typing rule to require the +relevant annotation. In the \texttt{version3} implementation, type signatures +in the environment now include an \cd{Epsilon} tag, and the function +\cd{checkStage} ensures that this tag is $[[Rel]]$ when the variable is used +in the term. \[ \drule{t-evar} \] An irrelevant abstraction introduces its variable into the context tagged with -the irrelevant annotation. Because of the $[[Irr]]$ tag, such variables are +the irrelevant annotation. Because of the $[[Irr]]$ tag, these variables are inaccessible in the body of the function. \[ @@ -1916,8 +1938,8 @@ in the \rref{t-eapp} rule below. \] This operation on the context, called \emph{resurrection}, converts all -$[[Irr]]$ tags on variables to be $[[Rel]]$. It represents a shift in our -perspective: because we have entered an irrelevant part of the term, the +``$[[Irr]]$'' tags on variables to be ``$[[Rel]]$''. It represents a shift in +our perspective: because we have entered an irrelevant part of the term, the variables that were not visible before are now available after this context modification. @@ -1951,7 +1973,7 @@ arguments are now tagged with their relevance, and when we compare arguments that are tagged as irrelevant, we do nothing. In fact, what we are doing is actually \emph{defining} equality over just the computationally relevant parts of the term instead of the entire term. And we have been doing this in a limited -form from the beginning---recall that \texttt{version1} of \pif \pif already +form from the beginning---recall that \texttt{version1} of \pif already ignores type annotations. Just as type annotations do not affect computation and can be ignored, the same reasoning holds for irrelevant arguments. diff --git a/doc/oplss.pdf b/doc/oplss.pdf index aca2861..214e9c8 100644 Binary files a/doc/oplss.pdf and b/doc/oplss.pdf differ diff --git a/doc/pi-rules.tex b/doc/pi-rules.tex index f4fe06a..adc793a 100644 --- a/doc/pi-rules.tex +++ b/doc/pi-rules.tex @@ -39,28 +39,22 @@ \ottprodline{|}{ - }{}{}{}{}} \newcommand{\ottv}{ -\ottrulehead{\ottnt{v}}{::=}{\ottcom{values and weak head normal forms}}\ottprodnewline +\ottrulehead{\ottnt{v}}{::=}{\ottcom{values}}\ottprodnewline \ottfirstprodline{|}{\ottkw{Type}}{}{}{}{}\ottprodnewline \ottprodline{|}{ \lambda \ottmv{x} . \ottnt{a} }{}{}{}{}\ottprodnewline \ottprodline{|}{ ( \ottmv{x} \!:\! \ottnt{A} ) \to \ottnt{B} }{}{}{}{}\ottprodnewline \ottprodline{|}{\ottkw{Unit}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottsym{()}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline -\ottprodline{|}{ \ottnt{ne} \; \ottnt{b} }{}{}{}{}\ottprodnewline \ottprodline{|}{\ottsym{(} \ottnt{v} \ottsym{)}} {\textsf{S}}{}{}{}\ottprodnewline \ottprodline{|}{ \{ \ottmv{x} \!:\! \ottnt{A} \ |\ \ottnt{B} \} }{}{}{}{}\ottprodnewline \ottprodline{|}{\ottsym{(} \ottnt{a} \ottsym{,} \ottnt{b} \ottsym{)}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottkw{let} \, \ottsym{(} \ottmv{x} \ottsym{,} \ottmv{y} \ottsym{)} \ottsym{=} \ottnt{ne} \, \ottkw{in} \, \ottnt{a}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottkw{Bool}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottkw{True}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottkw{False}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottkw{if} \, \ottnt{ne} \, \ottkw{then} \, \ottnt{a} \, \ottkw{else} \, \ottnt{b}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{a} \ottsym{=} \ottnt{b}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottkw{refl}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottmv{K} \, \overline{a}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottmv{T} \, \overline{a}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottkw{case} \, \ottnt{ne} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}} \to \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}} +\ottprodline{|}{\ottmv{T} \, \overline{a}}{}{}{}{}} \newcommand{\ottneutral}{ \ottrulehead{\ottnt{neutral} ,\ \ottnt{ne}}{::=}{\ottcom{neutral terms}}\ottprodnewline @@ -72,6 +66,30 @@ \ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottkw{case} \, \ottnt{ne} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}} \to \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}} +\newcommand{\ottnf}{ +\ottrulehead{\ottnt{nf}}{::=}{\ottcom{weak head normal forms}}\ottprodnewline +\ottfirstprodline{|}{\ottkw{Type}}{}{}{}{}\ottprodnewline +\ottprodline{|}{ \lambda \ottmv{x} . \ottnt{a} }{}{}{}{}\ottprodnewline +\ottprodline{|}{ ( \ottmv{x} \!:\! \ottnt{A} ) \to \ottnt{B} }{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{Unit}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{()}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline +\ottprodline{|}{ \ottnt{ne} \; \ottnt{b} }{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{(} \ottnt{nf} \ottsym{)}} {\textsf{S}}{}{}{}\ottprodnewline +\ottprodline{|}{ \{ \ottmv{x} \!:\! \ottnt{A} \ |\ \ottnt{B} \} }{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottsym{(} \ottnt{a} \ottsym{,} \ottnt{b} \ottsym{)}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{let} \, \ottsym{(} \ottmv{x} \ottsym{,} \ottmv{y} \ottsym{)} \ottsym{=} \ottnt{ne} \, \ottkw{in} \, \ottnt{a}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{Bool}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{True}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{False}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{if} \, \ottnt{ne} \, \ottkw{then} \, \ottnt{a} \, \ottkw{else} \, \ottnt{b}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{a} \ottsym{=} \ottnt{b}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{refl}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottmv{K} \, \overline{a}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottmv{T} \, \overline{a}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{case} \, \ottnt{ne} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}} \to \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}} + \newcommand{\ottargs}{ \ottrulehead{\overline{a} ,\ \overline{b}}{::=}{}\ottprodnewline \ottfirstprodline{|}{}{}{}{}{}\ottprodnewline @@ -159,6 +177,7 @@ \ottep\ottinterrule \ottv\ottinterrule \ottneutral\ottinterrule +\ottnf\ottinterrule \ottargs\ottinterrule \ottpat\ottinterrule \ottms\ottinterrule @@ -169,13 +188,69 @@ }} % defnss +% defns JEquate +%% defn equate +\newcommand{\ottdruleeqXXrefl}[1]{\ottdrule[#1]{% +}{ +\Gamma \vdash \ottnt{a} \Leftrightarrow \ottnt{a}}{% +{\ottdrulename{eq\_refl}}{}% +}} + + +\newcommand{\ottdruleeqXXwhnf}[1]{\ottdrule[#1]{% +\ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{nf_{{\mathrm{1}}}} }% +\ottpremise{ \ottkw{whnf} \ \ottnt{b} \leadsto \ottnt{nf_{{\mathrm{2}}}} }% +\ottpremise{\Gamma \vdash \ottnt{nf_{{\mathrm{1}}}} \Leftrightarrow \ottnt{nf_{{\mathrm{2}}}}}% +}{ +\Gamma \vdash \ottnt{a} \Leftrightarrow \ottnt{b}}{% +{\ottdrulename{eq\_whnf}}{}% +}} + + +\newcommand{\ottdruleeqXXabs}[1]{\ottdrule[#1]{% +\ottpremise{\Gamma \vdash \ottnt{a_{{\mathrm{1}}}} \Leftrightarrow \ottnt{a_{{\mathrm{2}}}}}% +}{ +\Gamma \vdash \lambda \ottmv{x} . \ottnt{a_{{\mathrm{1}}}} \Leftrightarrow \lambda \ottmv{x} . \ottnt{a_{{\mathrm{2}}}} }{% +{\ottdrulename{eq\_abs}}{}% +}} + + +\newcommand{\ottdruleeqXXpi}[1]{\ottdrule[#1]{% +\ottpremise{\Gamma \vdash \ottnt{A_{{\mathrm{1}}}} \Leftrightarrow \ottnt{A_{{\mathrm{2}}}}}% +\ottpremise{\Gamma \vdash \ottnt{B_{{\mathrm{1}}}} \Leftrightarrow \ottnt{B_{{\mathrm{2}}}}}% +}{ +\Gamma \vdash ( \ottmv{x} \!:\! \ottnt{A_{{\mathrm{1}}}} ) \to \ottnt{B_{{\mathrm{1}}}} \Leftrightarrow ( \ottmv{x} \!:\! \ottnt{A_{{\mathrm{2}}}} ) \to \ottnt{B_{{\mathrm{2}}}} }{% +{\ottdrulename{eq\_pi}}{}% +}} + + +\newcommand{\ottdruleeqXXapp}[1]{\ottdrule[#1]{% +\ottpremise{\Gamma \vdash \ottnt{ne_{{\mathrm{1}}}} \Leftrightarrow \ottnt{ne_{{\mathrm{2}}}}}% +\ottpremise{\Gamma \vdash \ottnt{b_{{\mathrm{1}}}} \Leftrightarrow \ottnt{b_{{\mathrm{2}}}}}% +}{ +\Gamma \vdash \ottnt{ne_{{\mathrm{1}}}} \; \ottnt{b_{{\mathrm{1}}}} \Leftrightarrow \ottnt{ne_{{\mathrm{2}}}} \; \ottnt{b_{{\mathrm{2}}}} }{% +{\ottdrulename{eq\_app}}{}% +}} + +\newcommand{\ottdefnequate}[1]{\begin{ottdefnblock}[#1]{$\Gamma \vdash \ottnt{a} \Leftrightarrow \ottnt{b}$}{} + compare $a$ and $b$ for equality \ottusedrule{\ottdruleeqXXrefl{}} +\ottusedrule{\ottdruleeqXXwhnf{}} +\ottusedrule{\ottdruleeqXXabs{}} +\ottusedrule{\ottdruleeqXXpi{}} +\ottusedrule{\ottdruleeqXXapp{}} +\end{ottdefnblock}} + + +\newcommand{\ottdefnsJEquate}{ +\ottdefnequate{}} + % defns Jwhnf %% defn whnf \newcommand{\ottdrulewhnfXXlamXXbeta}[1]{\ottdrule[#1]{% \ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottsym{(} \lambda \ottmv{x} . \ottnt{a'} \ottsym{)} }% -\ottpremise{ \ottkw{whnf} \ \ottsym{(} \ottnt{a'} \ottsym{[} \ottnt{b} \ottsym{/} \ottmv{x} \ottsym{]} \ottsym{)} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottsym{(} \ottnt{a'} \ottsym{[} \ottnt{b} \ottsym{/} \ottmv{x} \ottsym{]} \ottsym{)} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottnt{a} \; \ottnt{b} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottnt{a} \; \ottnt{b} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_lam\_beta}}{}% }} @@ -217,18 +292,18 @@ \newcommand{\ottdrulewhnfXXannot}[1]{\ottdrule[#1]{% -\ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottsym{(} \ottnt{a} \ottsym{:} \ottnt{A} \ottsym{)} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottsym{(} \ottnt{a} \ottsym{:} \ottnt{A} \ottsym{)} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_annot}}{}% }} \newcommand{\ottdrulewhnfXXletpair}[1]{\ottdrule[#1]{% \ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottsym{(} \ottnt{a_{{\mathrm{1}}}} \ottsym{,} \ottnt{a_{{\mathrm{2}}}} \ottsym{)} }% -\ottpremise{ \ottkw{whnf} \ \ottsym{(} \ottnt{b} \ottsym{[} \ottnt{a_{{\mathrm{1}}}} \ottsym{/} \ottmv{x} \ottsym{]} \ottsym{[} \ottnt{a_{{\mathrm{2}}}} \ottsym{/} \ottmv{y} \ottsym{]} \ottsym{)} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottsym{(} \ottnt{b} \ottsym{[} \ottnt{a_{{\mathrm{1}}}} \ottsym{/} \ottmv{x} \ottsym{]} \ottsym{[} \ottnt{a_{{\mathrm{2}}}} \ottsym{/} \ottmv{y} \ottsym{]} \ottsym{)} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottkw{let} \, \ottsym{(} \ottmv{x} \ottsym{,} \ottmv{y} \ottsym{)} \ottsym{=} \ottnt{a} \, \ottkw{in} \, \ottnt{b} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottkw{let} \, \ottsym{(} \ottmv{x} \ottsym{,} \ottmv{y} \ottsym{)} \ottsym{=} \ottnt{a} \, \ottkw{in} \, \ottnt{b} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_letpair}}{}% }} @@ -243,18 +318,18 @@ \newcommand{\ottdrulewhnfXXifXXtrue}[1]{\ottdrule[#1]{% \ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottkw{True} }% -\ottpremise{ \ottkw{whnf} \ \ottnt{b_{{\mathrm{1}}}} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottnt{b_{{\mathrm{1}}}} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottkw{if} \, \ottnt{a} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottkw{if} \, \ottnt{a} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_if\_true}}{}% }} \newcommand{\ottdrulewhnfXXifXXfalse}[1]{\ottdrule[#1]{% \ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottkw{False} }% -\ottpremise{ \ottkw{whnf} \ \ottnt{b_{{\mathrm{2}}}} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottnt{b_{{\mathrm{2}}}} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottkw{if} \, \ottnt{a} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottkw{if} \, \ottnt{a} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_if\_false}}{}% }} @@ -304,9 +379,9 @@ \newcommand{\ottdrulewhnfXXsubst}[1]{\ottdrule[#1]{% \ottpremise{ \ottkw{whnf} \ \ottnt{b} \leadsto \ottkw{refl} }% -\ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottsym{(} \ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{b} \ottsym{)} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottsym{(} \ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{b} \ottsym{)} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_subst}}{}% }} @@ -335,9 +410,9 @@ \newcommand{\ottdrulewhnfXXcase}[1]{\ottdrule[#1]{% \ottpremise{\ottkw{match} \, \ottsym{(} \ottmv{K} \, \overline{a} \ottsym{)} \ottsym{(pati} \to \ottsym{ai)} \leadsto \ottnt{b}}% -\ottpremise{ \ottkw{whnf} \ \ottnt{b} \leadsto \ottnt{v} }% +\ottpremise{ \ottkw{whnf} \ \ottnt{b} \leadsto \ottnt{nf} }% }{ - \ottkw{whnf} \ \ottkw{case} \, \ottsym{(} \ottmv{K} \, \overline{a} \ottsym{)} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}} \to \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}} \leadsto \ottnt{v} }{% + \ottkw{whnf} \ \ottkw{case} \, \ottsym{(} \ottmv{K} \, \overline{a} \ottsym{)} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}} \to \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}} \leadsto \ottnt{nf} }{% {\ottdrulename{whnf\_case}}{}% }} @@ -366,7 +441,7 @@ {\ottdrulename{whnf\_let\_beta}}{}% }} -\newcommand{\ottdefnwhnf}[1]{\begin{ottdefnblock}[#1]{$ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{v} $}{\ottcom{weak head normalize a to v (if possible)}} +\newcommand{\ottdefnwhnf}[1]{\begin{ottdefnblock}[#1]{$ \ottkw{whnf} \ \ottnt{a} \leadsto \ottnt{nf} $}{\ottcom{weak head normalize a to nf (if possible)}} \ottusedrule{\ottdrulewhnfXXlamXXbeta{}} \ottusedrule{\ottdrulewhnfXXtype{}} \ottusedrule{\ottdrulewhnfXXlam{}} @@ -1392,6 +1467,16 @@ }} +\newcommand{\ottdrulecXXwhnf}[1]{\ottdrule[#1]{% +\ottpremise{ \ottnt{A} \mbox{ is not in weak-head normal form } }% +\ottpremise{\Gamma \vdash \ottnt{a} \Leftarrow \ottnt{nf}}% +\ottpremise{ \ottkw{whnf} \ \ottnt{A} \leadsto \ottnt{nf} }% +}{ +\Gamma \vdash \ottnt{a} \Leftarrow \ottnt{A}}{% +{\ottdrulename{c\_whnf}}{}% +}} + + \newcommand{\ottdrulecXXpair}[1]{\ottdrule[#1]{% \ottpremise{\Gamma \vdash \ottnt{a} \Leftarrow \ottnt{A}}% \ottpremise{\Gamma \vdash \ottnt{b} \Leftarrow \ottnt{B} \ottsym{[} \ottnt{a} \ottsym{/} \ottmv{x} \ottsym{]}}% @@ -1564,6 +1649,7 @@ \ottusedrule{\ottdrulecXXlambda{}} \ottusedrule{\ottdrulecXXinferXXsimple{}} \ottusedrule{\ottdrulecXXinfer{}} +\ottusedrule{\ottdrulecXXwhnf{}} \ottusedrule{\ottdrulecXXpair{}} \ottusedrule{\ottdrulecXXletpairXXsimple{}} \ottusedrule{\ottdrulecXXletpair{}} @@ -1588,6 +1674,7 @@ \ottdefncheckCtx{}\ottdefntcArgTele{}\ottdefndeclarePats{}\ottdefndeclarePat{}\ottdefninferType{}\ottdefncheckType{}} \newcommand{\ottdefnss}{ +\ottdefnsJEquate \ottdefnsJwhnf \ottdefnsJOp \ottdefnsJEq diff --git a/doc/pi.ott b/doc/pi.ott index 75699d0..ec2f6b2 100644 --- a/doc/pi.ott +++ b/doc/pi.ott @@ -59,7 +59,7 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }} | () :: :: LitUnit {{ com unit term }} -v :: 'v_' ::= {{ com values and weak head normal forms }} +v :: 'v_' ::= {{ com values }} | Type :: :: Type @@ -71,13 +71,8 @@ v :: 'v_' ::= {{ com values and weak head normal forms }} | () :: :: LitUnit - | x :: :: Var - - | ne b :: :: App - | ( v ) :: S :: Paren - neutral, ne :: 'n_' ::= {{ com neutral terms }} | x :: :: Var @@ -86,9 +81,28 @@ neutral, ne :: 'n_' ::= {{ com neutral terms }} | ( ne ) :: S :: Paren +nf :: 'nf_' ::= {{ com weak head normal forms }} + + | Type :: :: Type + + | \ x . a :: :: Lam + + | ( x : A ) -> B :: :: Pi + + | Unit :: :: TyUnit + + | () :: :: LitUnit + + | x :: :: Var + + | ne b :: :: App + + | ( nf ) :: S :: Paren + subrules - ne <:: v - v <:: a + ne <:: nf + v <:: nf + nf <:: a substitutions single a x :: subst_tm @@ -157,6 +171,8 @@ formula :: 'formula_' ::= | G |- A <=> B :: :: equate | notlam a :: :: notlam {{ tex [[a]]\mbox{ is not a $\lambda$-expression } }} + | notwhnf a :: :: notwhnf + {{ tex [[a]]\mbox{ is not in weak-head normal form } }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -169,17 +185,17 @@ Jwhnf :: '' ::= % in our implementation. defn -whnf a ~> v :: :: whnf :: 'whnf_' -{{ tex [[whnf]]\ [[a]] \leadsto [[v]] }} -{{ com weak head normalize a to v (if possible) }} +whnf a ~> nf :: :: whnf :: 'whnf_' +{{ tex [[whnf]]\ [[a]] \leadsto [[nf]] }} +{{ com weak head normalize a to nf (if possible) }} by % reduction rules whnf a ~> (\x.a') -whnf (a'[b/x]) ~> v +whnf (a'[b/x]) ~> nf ---------------------- :: lam_beta -whnf a b ~> v +whnf a b ~> nf ------------------ :: type @@ -206,11 +222,51 @@ whnf a b ~> ne b % remove type annotations when normalizing % -whnf a ~> v +whnf a ~> nf ------------------ :: annot -whnf (a : A) ~> v +whnf (a : A) ~> nf +defns +JEquate :: '' ::= + +defn +G |- a <=> b :: :: equate :: 'eq_' +by +{{ com compare $a$ and $b$ for equality }} + +%% alpha-equivalent terms are equal + +---------------- :: refl +G |- a <=> a + + +%% if whnfs are equal, then the terms are equal + +whnf a ~> nf1 +whnf b ~> nf2 +G |- nf1 <=> nf2 +------------- :: whnf +G |- a <=> b + + +%% if terms are in whnf, compare subterms + +G |- a1 <=> a2 +--------------------------------- :: abs +G |- \x. a1 <=> \x. a2 + +G |- A1 <=> A2 +G |- B1 <=> B2 +-------------------------------- :: pi +G |- (x : A1) -> B1 <=> (x:A2) -> B2 + + +G |- ne1 <=> ne2 +G |- b1 <=> b2 +--------------------------------- :: app +G |- ne1 b1 <=> ne2 b2 + defns JOp :: '' ::= @@ -223,7 +279,6 @@ by (\x.a) b ~> a [ b / x] - a ~> a' ------------------------ :: app a b ~> a' b @@ -394,6 +449,11 @@ G |- A <=> B -------------------------- :: infer G |- a <= B +notwhnf A +G |- a <= nf +whnf A ~> nf +--------------- :: whnf +G |- a <= A defn |- G :: :: checkCtx :: 'g_' diff --git a/doc/sigma.ott b/doc/sigma.ott index bbc937d..48010f8 100644 --- a/doc/sigma.ott +++ b/doc/sigma.ott @@ -19,22 +19,27 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }} v :: 'v_' ::= | { x : A | B } :: :: Sigma | ( a , b ) :: :: Prod - | let ( x , y ) = ne in a :: :: LetPair neutral, ne :: 'n_' ::= | let ( x , y ) = ne in a :: :: LetPair +nf :: 'nf_' ::= + | { x : A | B } :: :: Sigma + | ( a , b ) :: :: Prod + | let ( x , y ) = ne in a :: :: LetPair + + defns Jwhnf :: '' ::= defn -whnf a ~> v :: :: whnf :: 'whnf_' +whnf a ~> nf :: :: whnf :: 'whnf_' by whnf a ~> (a1, a2) -whnf (b [a1/x] [a2/y]) ~> v +whnf (b [a1/x] [a2/y]) ~> nf ------------------------------- :: letpair -whnf let (x,y) = a in b ~> v +whnf let (x,y) = a in b ~> nf whnf a ~> ne --------------------------------------------- :: prodcong diff --git a/doc/template.ott b/doc/template.ott index f6ea2f0..6e3999c 100644 --- a/doc/template.ott +++ b/doc/template.ott @@ -9,7 +9,7 @@ defns Jwhnf :: '' ::= defn -whnf a = v :: :: whnf :: 'whnf_' +whnf a = nf :: :: whnf :: 'whnf_' by defns diff --git a/doc/tyeq.ott b/doc/tyeq.ott index 57cc4c3..12a1724 100644 --- a/doc/tyeq.ott +++ b/doc/tyeq.ott @@ -12,17 +12,22 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }} v :: 'v_' ::= | a = b :: :: TyEq | refl :: :: Refl - | subst a by ne :: :: Subst neutral, ne :: 'n_' ::= | subst a by ne :: :: Subst +nf :: 'nf_' ::= + | a = b :: :: TyEq + | refl :: :: Refl + | subst a by ne :: :: Subst + + defns Jwhnf :: '' ::= defn -whnf a ~> v :: :: whnf :: 'whnf_' -{{ tex whnf [[a]] \leadsto [[v]] }} +whnf a ~> nf :: :: whnf :: 'whnf_' +{{ tex whnf [[a]] \leadsto [[nf]] }} by ----------------------- :: tyeq @@ -34,9 +39,9 @@ whnf refl ~> refl whnf b ~> refl -whnf a ~> v +whnf a ~> nf ------------------------ :: subst -whnf (subst a by b) ~> v +whnf (subst a by b) ~> nf whnf b ~> ne ---------------------------------------- :: subst_cong diff --git a/full/src/Equal.hs b/full/src/Equal.hs index 0393f00..c5c9627 100644 --- a/full/src/Equal.hs +++ b/full/src/Equal.hs @@ -48,8 +48,10 @@ equate t1 t2 = do (LitBool b1, LitBool b2) | b1 == b2 -> return () - (If a1 b1 c1, If a2 b2 c2) -> - equate a1 a2 >> equate b1 b2 >> equate c1 c2 + (If a1 b1 c1, If a2 b2 c2) -> do + equate a1 a2 + equate b1 b2 + equate c1 c2 (Let rhs1 bnd1, Let rhs2 bnd2) -> do Just (x, body1, _, body2) <- Unbound.unbind2 bnd1 bnd2 @@ -228,9 +230,12 @@ whnf (Case scrut mtchs) = do -- don't do anything special for them whnf tm = return tm --- | 'Unify' the two terms, producing a list of Defs --- If there is an obvious mismatch, this function produces an error --- If either term is "ambiguous" just ignore. +-- | 'Unify' the two terms, producing a list of definitions that +-- must hold for the terms to be equal +-- If the terms are already equal, succeed with an empty list +-- If there is an obvious mismatch, fail with an error +-- If either term is "ambiguous" (i.e. neutral), give up and +-- succeed with an empty list unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx diff --git a/full/src/TypeCheck.hs b/full/src/TypeCheck.hs index 2e50cf1..66c1d73 100644 --- a/full/src/TypeCheck.hs +++ b/full/src/TypeCheck.hs @@ -9,7 +9,6 @@ import Data.List (nub) import Data.Maybe ( catMaybes ) - import Environment (D (..), TcMonad) import Environment qualified as Env import Equal qualified @@ -30,7 +29,7 @@ import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = case t of +inferType a = case a of -- i-var (Var x) -> do decl <- Env.lookupTy x -- make sure the variable is accessible @@ -48,30 +47,30 @@ inferType t = case t of return TyType -- i-app - (App t1 t2) -> do - ty1 <- inferType t1 + (App a b) -> do + ty1 <- inferType a let ensurePi = Equal.ensurePi (ep1, tyA, bnd) <- ensurePi ty1 - unless (ep1 == argEp t2) $ Env.err + unless (ep1 == argEp b) $ Env.err [DS "In application, expected", DD ep1, DS "argument but found", - DD t2, DS "instead." ] + DD b, DS "instead." ] -- if the argument is Irrelevant, resurrect the context (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ - checkType (unArg t2) tyA - return (Unbound.instantiate bnd [unArg t2]) + checkType (unArg b) tyA + return (Unbound.instantiate bnd [unArg b]) -- i-ann - (Ann tm ty) -> do - tcType ty - checkType tm ty - return ty + (Ann a tyA) -> do + tcType tyA + checkType a tyA + return tyA -- Practicalities -- remember the current position in the type checking monad - (Pos p tm) -> - Env.extendSourceLocation p tm $ inferType tm + (Pos p a) -> + Env.extendSourceLocation p a $ inferType a -- Extensions to the core language -- i-unit @@ -82,19 +81,14 @@ inferType t = case t of TyBool -> return TyType -- i-true/false - (LitBool b) -> return TyBool + (LitBool _) -> return TyBool -- i-if - (If t1 t2 t3) -> do - checkType t1 TyBool - ty <- inferType t2 - checkType t3 ty - return ty - -- i-eq - (TyEq a b) -> do - aTy <- inferType a - checkType b aTy - return TyType + (If a b1 b2) -> do + checkType a TyBool + tyA <- inferType b1 + checkType b2 tyA + return tyA -- i-sigma (TySigma tyA bnd) -> do @@ -102,6 +96,11 @@ inferType t = case t of tcType tyA Env.extendCtx (mkDecl x tyA) $ tcType tyB return TyType + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType -- Type constructor application (TyCon c params) -> do @@ -147,8 +146,8 @@ inferType t = case t of _ -> Env.err [DS "Ambiguous data constructor", DS c] -- cannot synthesize the type of the term - tm -> - Env.err [DS "Must have a type for", DD tm] + _ -> + Env.err [DS "Must have a type annotation for", DD a] ------------------------------------------------------------------------- @@ -160,52 +159,117 @@ tcType tm = Env.withStage Irr $ checkType tm TyType ------------------------------------------------------------------------- -- | Check that the given term has the expected type checkType :: Term -> Type -> TcMonad () -checkType tm ty' = do - ty <- Equal.whnf ty' +checkType tm ty = do + ty' <- Equal.whnf ty case tm of -- c-lam: check the type of a function - (Lam ep1 bnd) -> case ty of + (Lam ep1 bnd) -> case ty' of (TyPi ep2 tyA bnd2) -> do -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 + (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 -- epsilons should match up unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, DS "but found", DD ep1, DS "instead."] -- check the type of the body of the lambda expression Env.extendCtx (Decl (TypeDecl x ep1 tyA)) (checkType body tyB) - _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty'] -- Practicalities - (Pos p tm) -> - Env.extendSourceLocation p tm $ checkType tm ty + (Pos p a) -> + Env.extendSourceLocation p a $ checkType a ty' TrustMe -> return () PrintMe -> do gamma <- Env.getLocalCtx Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] + DS "\nGoal:", DD ty'] -- Extensions to the core language -- c-if - (If t1 t2 t3) -> do - checkType t1 TyBool - dtrue <- Equal.unify [] t1 (LitBool True) - dfalse <- Equal.unify [] t1 (LitBool False) - Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - + (If a b1 b2) -> do + checkType a TyBool + dtrue <- Equal.unify [] a (LitBool True) + dfalse <- Equal.unify [] a (LitBool False) + Env.extendCtxs dtrue $ checkType b1 ty' + Env.extendCtxs dfalse $ checkType b2 ty' + -- c-prod + (Prod a b) -> do + case ty' of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + + -- c-letpair + (LetPair p bnd) -> do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body tyA + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + -- c-let - (Let rhs bnd) -> do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - Env.extendCtxs [mkDecl x aty, Def x rhs] $ - checkType body ty + (Let a bnd) -> do + (x, b) <- Unbound.unbind bnd + tyA <- inferType a + Env.extendCtxs [mkDecl x tyA, Def x a] $ + checkType b ty' + -- c-refl + Refl -> case ty' of + (TyEq a b) -> Equal.equate a b + _ -> Env.err [DS "Refl annotated with invalid type", DD ty'] + -- c-subst + (Subst a b) -> do + -- infer the type of the proof 'b' + tp <- inferType b + -- make sure that it is an equality between m and n + (m, n) <- Equal.ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- Equal.unify [] m n + -- if proof is a variable, add a definition to the context + pdecl <- Equal.unify [] b Refl + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty' + -- c-contra + (Contra p) -> do + ty' <- inferType p + (a, b) <- Equal.ensureTyEq ty' + a' <- Equal.whnf a + b' <- Equal.whnf b + case (a', b') of + + (DataCon da _, DataCon db _) + | da /= db -> + return () + + (LitBool b1, LitBool b2) + | b1 /= b2 -> + return () + (_, _) -> + Env.err + [ DS "I can't tell that", + DD a, + DS "and", + DD b, + DS "are contradictory" + ] + -- c-data -- we know the expected type of the data constructor -- so look up its type in the context (DataCon c args) -> do - case ty of + case ty' of (TyCon tname params) -> do (Telescope delta, Telescope deltai) <- Env.lookupDCon c tname let isDecl :: Entry -> Bool @@ -225,7 +289,7 @@ checkType tm ty' = do newTele <- substTele delta params deltai tcArgTele args newTele _ -> - Env.err [DS "Unexpected type", DD ty, DS "for data constructor", DD tm] + Env.err [DS "Unexpected type", DD ty', DS "for data constructor", DD tm] (Case scrut alts) -> do sty <- inferType scrut @@ -239,86 +303,19 @@ checkType tm ty' = do -- add defs to the contents from scrut = pat -- could fail if branch is in-accessible decls' <- Equal.unify [] scrut' (pat2Term pat) - Env.extendCtxs (decls ++ decls') $ checkType body ty + Env.extendCtxs (decls ++ decls') $ checkType body ty' return () let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts mapM_ checkAlt alts exhaustivityCheck scrut' sty pats - -- c-refl - Refl -> case ty of - (TyEq a b) -> Equal.equate a b - _ -> Env.err [DS "Refl annotated with", DD ty] - -- c-subst - (Subst a b) -> do - -- infer the type of the proof 'b' - tp <- inferType b - -- make sure that it is an equality between m and n - (m, n) <- Equal.ensureTyEq tp - -- if either side is a variable, add a definition to the context - edecl <- Equal.unify [] m n - -- if proof is a variable, add a definition to the context - pdecl <- Equal.unify [] b Refl - Env.extendCtxs (edecl ++ pdecl) $ checkType a ty - -- c-contra - (Contra p) -> do - ty' <- inferType p - (a, b) <- Equal.ensureTyEq ty' - a' <- Equal.whnf a - b' <- Equal.whnf b - case (a', b') of - - (DataCon da _, DataCon db _) - | da /= db -> - return () - - (LitBool b1, LitBool b2) - | b1 /= b2 -> - return () - (_, _) -> - Env.err - [ DS "I can't tell that", - DD a, - DS "and", - DD b, - DS "are contradictory" - ] - - -- c-prod - (Prod a b) -> do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - - - -- c-letpair - (LetPair p bnd) -> do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ - checkType body ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] - -- c-infer - tm -> do - ty' <- inferType tm - Equal.equate ty' ty + a -> do + tyA <- inferType a + Equal.equate tyA ty' --------------------------------------------------------------------- diff --git a/main/src/Equal.hs b/main/src/Equal.hs index 447937d..eb20ad1 100644 --- a/main/src/Equal.hs +++ b/main/src/Equal.hs @@ -50,8 +50,10 @@ equate t1 t2 = do (LitBool b1, LitBool b2) | b1 == b2 -> return () - (If a1 b1 c1, If a2 b2 c2) -> - equate a1 a2 >> equate b1 b2 >> equate c1 c2 + (If a1 b1 c1, If a2 b2 c2) -> do + equate a1 a2 + equate b1 b2 + equate c1 c2 (Let rhs1 bnd1, Let rhs2 bnd2) -> do Just (x, body1, _, body2) <- Unbound.unbind2 bnd1 bnd2 @@ -239,9 +241,12 @@ whnf (Case scrut mtchs) = do -- don't do anything special for them whnf tm = return tm --- | 'Unify' the two terms, producing a list of Defs --- If there is an obvious mismatch, this function produces an error --- If either term is "ambiguous" just ignore. +-- | 'Unify' the two terms, producing a list of definitions that +-- must hold for the terms to be equal +-- If the terms are already equal, succeed with an empty list +-- If there is an obvious mismatch, fail with an error +-- If either term is "ambiguous" (i.e. neutral), give up and +-- succeed with an empty list unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx diff --git a/main/src/TypeCheck.hs b/main/src/TypeCheck.hs index 23947a1..82d2995 100644 --- a/main/src/TypeCheck.hs +++ b/main/src/TypeCheck.hs @@ -10,7 +10,6 @@ import Data.List (nub) {- STUBWITH -} import Data.Maybe ( catMaybes ) - import Environment (D (..), TcMonad) import Environment qualified as Env import Equal qualified @@ -32,7 +31,7 @@ import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = case t of +inferType a = case a of -- i-var (Var x) -> do decl <- Env.lookupTy x {- SOLN EP -} @@ -51,8 +50,8 @@ inferType t = case t of return TyType -- i-app - (App t1 t2) -> do - ty1 <- inferType t1 + (App a b) -> do + ty1 <- inferType a {- SOLN EQUAL -} let ensurePi = Equal.ensurePi {- STUBWITH @@ -64,29 +63,29 @@ inferType t = case t of ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty] -} {- SOLN EP -} (ep1, tyA, bnd) <- ensurePi ty1 - unless (ep1 == argEp t2) $ Env.err + unless (ep1 == argEp b) $ Env.err [DS "In application, expected", DD ep1, DS "argument but found", - DD t2, DS "instead." ] + DD b, DS "instead." ] -- if the argument is Irrelevant, resurrect the context (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ - checkType (unArg t2) tyA - return (Unbound.instantiate bnd [unArg t2]) + checkType (unArg b) tyA + return (Unbound.instantiate bnd [unArg b]) {- STUBWITH (tyA,bnd) <- ensurePi ty1 - checkType t2 tyA - return (Unbound.instantiate bnd [t2]) -} + checkType b tyA + return (Unbound.instantiate bnd [b]) -} -- i-ann - (Ann tm ty) -> do - tcType ty - checkType tm ty - return ty + (Ann a tyA) -> do + tcType tyA + checkType a tyA + return tyA -- Practicalities -- remember the current position in the type checking monad - (Pos p tm) -> - Env.extendSourceLocation p tm $ inferType tm + (Pos p a) -> + Env.extendSourceLocation p a $ inferType a -- Extensions to the core language -- i-unit @@ -97,20 +96,14 @@ inferType t = case t of TyBool -> {- SOLN HW -} return TyType {- STUBWITH Env.err [DS "unimplemented"] -} -- i-true/false - (LitBool b) -> {- SOLN HW -} return TyBool {- STUBWITH Env.err [DS "unimplemented"] -} + (LitBool _) -> {- SOLN HW -} return TyBool {- STUBWITH Env.err [DS "unimplemented"] -} -- i-if - (If t1 t2 t3) -> {- SOLN HW -} do - checkType t1 TyBool - ty <- inferType t2 - checkType t3 ty - return ty {- STUBWITH Env.err [DS "unimplemented"] -} -{- SOLN EQUAL -} - -- i-eq - (TyEq a b) -> do - aTy <- inferType a - checkType b aTy - return TyType {- STUBWITH -} + (If a b1 b2) -> {- SOLN HW -} do + checkType a TyBool + tyA <- inferType b1 + checkType b2 tyA + return tyA {- STUBWITH Env.err [DS "unimplemented"] -} -- i-sigma (TySigma tyA bnd) -> {- SOLN EQUAL -} do @@ -118,6 +111,12 @@ inferType t = case t of tcType tyA Env.extendCtx (mkDecl x tyA) $ tcType tyB return TyType {- STUBWITH Env.err [DS "unimplemented"] -} +{- SOLN EQUAL -} + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType {- STUBWITH -} {- SOLN DATA -} -- Type constructor application @@ -164,8 +163,8 @@ inferType t = case t of _ -> Env.err [DS "Ambiguous data constructor", DS c] {- STUBWITH -} -- cannot synthesize the type of the term - tm -> - Env.err [DS "Must have a type for", DD tm] + _ -> + Env.err [DS "Must have a type annotation for", DD a] ------------------------------------------------------------------------- @@ -177,54 +176,122 @@ tcType tm = {- SOLN EP -} Env.withStage Irr $ {- STUBWITH -} checkType tm TyType ------------------------------------------------------------------------- -- | Check that the given term has the expected type checkType :: Term -> Type -> TcMonad () -checkType tm ty' = do +checkType tm ty = do {- SOLN EQUAL -} - ty <- Equal.whnf ty' {- STUBWITH let ty = strip ty' -- ignore source positions/annotations -} + ty' <- Equal.whnf ty {- STUBWITH let ty' = strip ty -- ignore source positions/annotations -} case tm of -- c-lam: check the type of a function - (Lam {- SOLN EP -} ep1 {- STUBWITH -} bnd) -> case ty of + (Lam {- SOLN EP -} ep1 {- STUBWITH -} bnd) -> case ty' of (TyPi {- SOLN EP -} ep2 {- STUBWITH -}tyA bnd2) -> do -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 + (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 {- SOLN EP -} -- epsilons should match up unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, DS "but found", DD ep1, DS "instead."] {- STUBWITH -} -- check the type of the body of the lambda expression Env.extendCtx {- SOLN EP -} (Decl (TypeDecl x ep1 tyA)){- STUBWITH (mkDecl x tyA) -} (checkType body tyB) - _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty'] -- Practicalities - (Pos p tm) -> - Env.extendSourceLocation p tm $ checkType tm ty + (Pos p a) -> + Env.extendSourceLocation p a $ checkType a ty' TrustMe -> return () PrintMe -> do gamma <- Env.getLocalCtx Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] + DS "\nGoal:", DD ty'] -- Extensions to the core language -- c-if - (If t1 t2 t3) -> {- SOLN HW -} do - checkType t1 TyBool - dtrue <- Equal.unify [] t1 (LitBool True) - dfalse <- Equal.unify [] t1 (LitBool False) - Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty {- STUBWITH Env.err [DS "unimplemented"] -} - + (If a b1 b2) -> {- SOLN HW -} do + checkType a TyBool + dtrue <- Equal.unify [] a (LitBool True) + dfalse <- Equal.unify [] a (LitBool False) + Env.extendCtxs dtrue $ checkType b1 ty' + Env.extendCtxs dfalse $ checkType b2 ty' {- STUBWITH Env.err [DS "unimplemented"] -} + -- c-prod + (Prod a b) -> {- SOLN EQUAL -} do + case ty' of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + {- STUBWITH Env.err [DS "unimplemented"] -} + -- c-letpair + (LetPair p bnd) -> {- SOLN EQUAL -} do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body tyA + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + {- STUBWITH Env.err [DS "unimplemented"] -} -- c-let - (Let rhs bnd) -> {- SOLN HW -} do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - Env.extendCtxs [mkDecl x aty, Def x rhs] $ - checkType body ty {- STUBWITH Env.err [DS "unimplemented"] -} + (Let a bnd) -> {- SOLN HW -} do + (x, b) <- Unbound.unbind bnd + tyA <- inferType a + Env.extendCtxs [mkDecl x tyA, Def x a] $ + checkType b ty' {- STUBWITH Env.err [DS "unimplemented"] -} +{- SOLN EQUAL -} + -- c-refl + Refl -> case ty' of + (TyEq a b) -> Equal.equate a b + _ -> Env.err [DS "Refl annotated with invalid type", DD ty'] + -- c-subst + (Subst a b) -> do + -- infer the type of the proof 'b' + tp <- inferType b + -- make sure that it is an equality between m and n + (m, n) <- Equal.ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- Equal.unify [] m n + -- if proof is a variable, add a definition to the context + pdecl <- Equal.unify [] b Refl + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty' + -- c-contra + (Contra p) -> do + ty' <- inferType p + (a, b) <- Equal.ensureTyEq ty' + a' <- Equal.whnf a + b' <- Equal.whnf b + case (a', b') of + {- STUBWITH -} +{- SOLN DATA -} + (DataCon da _, DataCon db _) + | da /= db -> + return () + {- STUBWITH -} +{- SOLN EQUAL -} + (LitBool b1, LitBool b2) + | b1 /= b2 -> + return () + (_, _) -> + Env.err + [ DS "I can't tell that", + DD a, + DS "and", + DD b, + DS "are contradictory" + ] + {- STUBWITH -} {- SOLN DATA -} -- c-data -- we know the expected type of the data constructor -- so look up its type in the context (DataCon c args) -> do - case ty of + case ty' of (TyCon tname params) -> do (Telescope delta, Telescope deltai) <- Env.lookupDCon c tname let isDecl :: Entry -> Bool @@ -244,7 +311,7 @@ checkType tm ty' = do newTele <- substTele delta params deltai tcArgTele args newTele _ -> - Env.err [DS "Unexpected type", DD ty, DS "for data constructor", DD tm] + Env.err [DS "Unexpected type", DD ty', DS "for data constructor", DD tm] (Case scrut alts) -> do sty <- inferType scrut @@ -258,91 +325,21 @@ checkType tm ty' = do -- add defs to the contents from scrut = pat -- could fail if branch is in-accessible decls' <- Equal.unify [] scrut' (pat2Term pat) - Env.extendCtxs (decls ++ decls') $ checkType body ty + Env.extendCtxs (decls ++ decls') $ checkType body ty' return () let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts mapM_ checkAlt alts exhaustivityCheck scrut' sty pats {- STUBWITH -} -{- SOLN EQUAL -} - -- c-refl - Refl -> case ty of - (TyEq a b) -> Equal.equate a b - _ -> Env.err [DS "Refl annotated with", DD ty] - -- c-subst - (Subst a b) -> do - -- infer the type of the proof 'b' - tp <- inferType b - -- make sure that it is an equality between m and n - (m, n) <- Equal.ensureTyEq tp - -- if either side is a variable, add a definition to the context - edecl <- Equal.unify [] m n - -- if proof is a variable, add a definition to the context - pdecl <- Equal.unify [] b Refl - Env.extendCtxs (edecl ++ pdecl) $ checkType a ty - -- c-contra - (Contra p) -> do - ty' <- inferType p - (a, b) <- Equal.ensureTyEq ty' - a' <- Equal.whnf a - b' <- Equal.whnf b - case (a', b') of - {- STUBWITH -} -{- SOLN DATA -} - (DataCon da _, DataCon db _) - | da /= db -> - return () - {- STUBWITH -} -{- SOLN EQUAL -} - (LitBool b1, LitBool b2) - | b1 /= b2 -> - return () - (_, _) -> - Env.err - [ DS "I can't tell that", - DD a, - DS "and", - DD b, - DS "are contradictory" - ] - {- STUBWITH -} - -- c-prod - (Prod a b) -> {- SOLN EQUAL -} do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - {- STUBWITH Env.err [DS "unimplemented"] -} - - -- c-letpair - (LetPair p bnd) -> {- SOLN EQUAL -} do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ - checkType body ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] - {- STUBWITH Env.err [DS "unimplemented"] -} -- c-infer - tm -> do - ty' <- inferType tm + a -> do + tyA <- inferType a {- SOLN EQUAL -} - Equal.equate ty' ty - {- STUBWITH unless (Unbound.aeq ty' ty) $ Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] -} + Equal.equate tyA ty' + {- STUBWITH unless (Unbound.aeq tyA ty') $ Env.err [DS "Types don't match", DD tyA, DS "and", DD ty'] -} {- SOLN DATA -} --------------------------------------------------------------------- diff --git a/version1/src/Equal.hs b/version1/src/Equal.hs index b92c8cd..8708685 100644 --- a/version1/src/Equal.hs +++ b/version1/src/Equal.hs @@ -44,8 +44,10 @@ equate t1 t2 = do (LitUnit, LitUnit) -> return () (TyBool, TyBool) -> return () (LitBool b1, LitBool b2) | b1 == b2 -> return () - (If a1 b1 c1, If a2 b2 c2) -> - equate a1 a2 >> equate b1 b2 >> equate c1 c2 + (If a1 b1 c1, If a2 b2 c2) -> do + equate a1 a2 + equate b1 b2 + equate c1 c2 (Let rhs1 bnd1, Let rhs2 bnd2) -> do Just (x, body1, _, body2) <- Unbound.unbind2 bnd1 bnd2 equate rhs1 rhs2 @@ -125,9 +127,12 @@ whnf (Pos _ tm) = whnf tm -- don't do anything special for them whnf tm = return tm --- | 'Unify' the two terms, producing a list of Defs --- If there is an obvious mismatch, this function produces an error --- If either term is "ambiguous" just ignore. +-- | 'Unify' the two terms, producing a list of definitions that +-- must hold for the terms to be equal +-- If the terms are already equal, succeed with an empty list +-- If there is an obvious mismatch, fail with an error +-- If either term is "ambiguous" (i.e. neutral), give up and +-- succeed with an empty list unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx diff --git a/version1/src/TypeCheck.hs b/version1/src/TypeCheck.hs index 0a7fd81..abf5ada 100644 --- a/version1/src/TypeCheck.hs +++ b/version1/src/TypeCheck.hs @@ -21,7 +21,7 @@ import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = case t of +inferType a = case a of -- i-var (Var x) -> do decl <- Env.lookupTy x @@ -37,27 +37,27 @@ inferType t = case t of return TyType -- i-app - (App t1 t2) -> do - ty1 <- inferType t1 + (App a b) -> do + ty1 <- inferType a let ensurePi :: Type -> TcMonad (Type, Unbound.Bind TName Type) ensurePi (Pos _ ty) = ensurePi ty ensurePi (Ann tm _) = ensurePi tm ensurePi (TyPi tyA bnd) = return (tyA, bnd) ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty] (tyA, bnd) <- ensurePi ty1 - checkType t2 tyA - return (Unbound.instantiate bnd [t2]) + checkType b tyA + return (Unbound.instantiate bnd [b]) -- i-ann - (Ann tm ty) -> do - tcType ty - checkType tm ty - return ty + (Ann a tyA) -> do + tcType tyA + checkType a tyA + return tyA -- Practicalities -- remember the current position in the type checking monad - (Pos p tm) -> - Env.extendSourceLocation p tm $ inferType tm + (Pos p a) -> + Env.extendSourceLocation p a $ inferType a -- Extensions to the core language -- i-unit TyUnit -> return TyType @@ -65,14 +65,14 @@ inferType t = case t of -- i-bool TyBool -> Env.err [DS "unimplemented"] -- i-true/false - (LitBool b) -> Env.err [DS "unimplemented"] + (LitBool _) -> Env.err [DS "unimplemented"] -- i-if - (If t1 t2 t3) -> Env.err [DS "unimplemented"] + (If a b1 b2) -> Env.err [DS "unimplemented"] -- i-sigma (TySigma tyA bnd) -> Env.err [DS "unimplemented"] -- cannot synthesize the type of the term - tm -> - Env.err [DS "Must have a type for", DD tm] + _ -> + Env.err [DS "Must have a type annotation for", DD a] ------------------------------------------------------------------------- @@ -84,21 +84,21 @@ tcType tm = checkType tm TyType -- | Check that the given term has the expected type checkType :: Term -> Type -> TcMonad () -checkType tm ty' = do - let ty = strip ty' -- ignore source positions/annotations +checkType tm ty = do + let ty' = strip ty -- ignore source positions/annotations case tm of -- c-lam: check the type of a function - (Lam bnd) -> case ty of + (Lam bnd) -> case ty' of (TyPi tyA bnd2) -> do -- unbind the variables in the lambda expression and pi type (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 -- check the type of the body of the lambda expression Env.extendCtx (mkDecl x tyA) (checkType body tyB) - _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty'] -- Practicalities - (Pos p tm) -> - Env.extendSourceLocation p tm $ checkType tm ty + (Pos p a) -> + Env.extendSourceLocation p a $ checkType a ty' TrustMe -> return () PrintMe -> do gamma <- Env.getLocalCtx @@ -106,22 +106,22 @@ checkType tm ty' = do [ DS "Unmet obligation.\nContext:", DD gamma, DS "\nGoal:", - DD ty + DD ty' ] -- Extensions to the core language -- c-if - (If t1 t2 t3) -> Env.err [DS "unimplemented"] - -- c-let - (Let rhs bnd) -> Env.err [DS "unimplemented"] + (If a b1 b2) -> Env.err [DS "unimplemented"] -- c-prod (Prod a b) -> Env.err [DS "unimplemented"] -- c-letpair (LetPair p bnd) -> Env.err [DS "unimplemented"] + -- c-let + (Let a bnd) -> Env.err [DS "unimplemented"] -- c-infer - tm -> do - ty' <- inferType tm - unless (Unbound.aeq ty' ty) $ Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] + a -> do + tyA <- inferType a + unless (Unbound.aeq tyA ty') $ Env.err [DS "Types don't match", DD tyA, DS "and", DD ty'] -------------------------------------------------------- -- Using the typechecker for decls and modules and stuff diff --git a/version2/pi/Lec1.pi b/version2/pi/Lec1.pi index eb6a040..2b5034e 100644 --- a/version2/pi/Lec1.pi +++ b/version2/pi/Lec1.pi @@ -48,7 +48,7 @@ unit = (x:Type) -> x -> x -- includes beta-equivalence/definitions (i.e. >= version2) -- Church encoding of simply-typed pairs -{- + pair : Type -> Type -> Type pair = \p. \q. (c: Type) -> (p -> q -> c) -> c @@ -56,6 +56,12 @@ pair = \p. \q. (c: Type) -> (p -> q -> c) -> c prod : (p:Type) -> (q:Type) -> p -> q -> pair p q prod = \p.\q. \x.\y. \c. \f. f x y +-- (p:Type) -> (q:Type) -> p -> q -> pair p q +-- (p:Type) -> (q:Type) -> p -> q -> ((c: Type) -> (p -> q -> c) -> c) + +prod' : (p:Type) -> (q:Type) -> p -> q -> ((c: Type) -> (p -> q -> c) -> c) +prod' = prod + proj1 : (p:Type) -> (q:Type) -> pair p q -> p proj1 = \p. \q. \a. a p (\x.\y.x) @@ -64,4 +70,4 @@ proj2 = \p. \q. \a. a q (\x.\y.y) swap : (p:Type) -> (q:Type) -> pair p q -> pair q p swap = \p. \q. \a. prod q p (proj2 p q a) (proj1 p q a) --} + diff --git a/version2/src/Equal.hs b/version2/src/Equal.hs index d91dd5a..3866dbb 100644 --- a/version2/src/Equal.hs +++ b/version2/src/Equal.hs @@ -46,8 +46,10 @@ equate t1 t2 = do (LitBool b1, LitBool b2) | b1 == b2 -> return () - (If a1 b1 c1, If a2 b2 c2) -> - equate a1 a2 >> equate b1 b2 >> equate c1 c2 + (If a1 b1 c1, If a2 b2 c2) -> do + equate a1 a2 + equate b1 b2 + equate c1 c2 (Let rhs1 bnd1, Let rhs2 bnd2) -> do Just (x, body1, _, body2) <- Unbound.unbind2 bnd1 bnd2 @@ -169,9 +171,12 @@ whnf (Subst tm pf) = do -- don't do anything special for them whnf tm = return tm --- | 'Unify' the two terms, producing a list of Defs --- If there is an obvious mismatch, this function produces an error --- If either term is "ambiguous" just ignore. +-- | 'Unify' the two terms, producing a list of definitions that +-- must hold for the terms to be equal +-- If the terms are already equal, succeed with an empty list +-- If there is an obvious mismatch, fail with an error +-- If either term is "ambiguous" (i.e. neutral), give up and +-- succeed with an empty list unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx diff --git a/version2/src/TypeCheck.hs b/version2/src/TypeCheck.hs index 8b5e965..fc0406a 100644 --- a/version2/src/TypeCheck.hs +++ b/version2/src/TypeCheck.hs @@ -8,7 +8,6 @@ import Control.Monad.Except import Data.Maybe ( catMaybes ) - import Environment (D (..), TcMonad) import Environment qualified as Env import Equal qualified @@ -28,7 +27,7 @@ import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = case t of +inferType a = case a of -- i-var (Var x) -> do decl <- Env.lookupTy x @@ -45,24 +44,24 @@ inferType t = case t of return TyType -- i-app - (App t1 t2) -> do - ty1 <- inferType t1 + (App a b) -> do + ty1 <- inferType a let ensurePi = Equal.ensurePi (tyA,bnd) <- ensurePi ty1 - checkType t2 tyA - return (Unbound.instantiate bnd [t2]) + checkType b tyA + return (Unbound.instantiate bnd [b]) -- i-ann - (Ann tm ty) -> do - tcType ty - checkType tm ty - return ty + (Ann a tyA) -> do + tcType tyA + checkType a tyA + return tyA -- Practicalities -- remember the current position in the type checking monad - (Pos p tm) -> - Env.extendSourceLocation p tm $ inferType tm + (Pos p a) -> + Env.extendSourceLocation p a $ inferType a -- Extensions to the core language -- i-unit @@ -73,19 +72,14 @@ inferType t = case t of TyBool -> return TyType -- i-true/false - (LitBool b) -> return TyBool + (LitBool _) -> return TyBool -- i-if - (If t1 t2 t3) -> do - checkType t1 TyBool - ty <- inferType t2 - checkType t3 ty - return ty - -- i-eq - (TyEq a b) -> do - aTy <- inferType a - checkType b aTy - return TyType + (If a b1 b2) -> do + checkType a TyBool + tyA <- inferType b1 + checkType b2 tyA + return tyA -- i-sigma (TySigma tyA bnd) -> do @@ -93,12 +87,17 @@ inferType t = case t of tcType tyA Env.extendCtx (mkDecl x tyA) $ tcType tyB return TyType + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType -- cannot synthesize the type of the term - tm -> - Env.err [DS "Must have a type for", DD tm] + _ -> + Env.err [DS "Must have a type annotation for", DD a] ------------------------------------------------------------------------- @@ -110,50 +109,75 @@ tcType tm = checkType tm TyType ------------------------------------------------------------------------- -- | Check that the given term has the expected type checkType :: Term -> Type -> TcMonad () -checkType tm ty' = do - ty <- Equal.whnf ty' +checkType tm ty = do + ty' <- Equal.whnf ty case tm of -- c-lam: check the type of a function - (Lam bnd) -> case ty of + (Lam bnd) -> case ty' of (TyPi tyA bnd2) -> do -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 + (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 -- check the type of the body of the lambda expression Env.extendCtx (mkDecl x tyA) (checkType body tyB) - _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty'] -- Practicalities - (Pos p tm) -> - Env.extendSourceLocation p tm $ checkType tm ty + (Pos p a) -> + Env.extendSourceLocation p a $ checkType a ty' TrustMe -> return () PrintMe -> do gamma <- Env.getLocalCtx Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] + DS "\nGoal:", DD ty'] -- Extensions to the core language -- c-if - (If t1 t2 t3) -> do - checkType t1 TyBool - dtrue <- Equal.unify [] t1 (LitBool True) - dfalse <- Equal.unify [] t1 (LitBool False) - Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - + (If a b1 b2) -> do + checkType a TyBool + dtrue <- Equal.unify [] a (LitBool True) + dfalse <- Equal.unify [] a (LitBool False) + Env.extendCtxs dtrue $ checkType b1 ty' + Env.extendCtxs dfalse $ checkType b2 ty' + -- c-prod + (Prod a b) -> do + case ty' of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + + -- c-letpair + (LetPair p bnd) -> do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body tyA + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + -- c-let - (Let rhs bnd) -> do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - Env.extendCtxs [mkDecl x aty, Def x rhs] $ - checkType body ty - + (Let a bnd) -> do + (x, b) <- Unbound.unbind bnd + tyA <- inferType a + Env.extendCtxs [mkDecl x tyA, Def x a] $ + checkType b ty' -- c-refl - Refl -> case ty of + Refl -> case ty' of (TyEq a b) -> Equal.equate a b - _ -> Env.err [DS "Refl annotated with", DD ty] + _ -> Env.err [DS "Refl annotated with invalid type", DD ty'] -- c-subst (Subst a b) -> do -- infer the type of the proof 'b' @@ -164,7 +188,7 @@ checkType tm ty' = do edecl <- Equal.unify [] m n -- if proof is a variable, add a definition to the context pdecl <- Equal.unify [] b Refl - Env.extendCtxs (edecl ++ pdecl) $ checkType a ty + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty' -- c-contra (Contra p) -> do ty' <- inferType p @@ -186,40 +210,13 @@ checkType tm ty' = do DS "are contradictory" ] - -- c-prod - (Prod a b) -> do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - - -- c-letpair - (LetPair p bnd) -> do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ - checkType body ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] - -- c-infer - tm -> do - ty' <- inferType tm - Equal.equate ty' ty + a -> do + tyA <- inferType a + Equal.equate tyA ty' diff --git a/version3/src/Equal.hs b/version3/src/Equal.hs index e33092e..6c274e8 100644 --- a/version3/src/Equal.hs +++ b/version3/src/Equal.hs @@ -48,8 +48,10 @@ equate t1 t2 = do (LitBool b1, LitBool b2) | b1 == b2 -> return () - (If a1 b1 c1, If a2 b2 c2) -> - equate a1 a2 >> equate b1 b2 >> equate c1 c2 + (If a1 b1 c1, If a2 b2 c2) -> do + equate a1 a2 + equate b1 b2 + equate c1 c2 (Let rhs1 bnd1, Let rhs2 bnd2) -> do Just (x, body1, _, body2) <- Unbound.unbind2 bnd1 bnd2 @@ -191,9 +193,12 @@ whnf (Subst tm pf) = do -- don't do anything special for them whnf tm = return tm --- | 'Unify' the two terms, producing a list of Defs --- If there is an obvious mismatch, this function produces an error --- If either term is "ambiguous" just ignore. +-- | 'Unify' the two terms, producing a list of definitions that +-- must hold for the terms to be equal +-- If the terms are already equal, succeed with an empty list +-- If there is an obvious mismatch, fail with an error +-- If either term is "ambiguous" (i.e. neutral), give up and +-- succeed with an empty list unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx diff --git a/version3/src/TypeCheck.hs b/version3/src/TypeCheck.hs index 69a5920..a416c79 100644 --- a/version3/src/TypeCheck.hs +++ b/version3/src/TypeCheck.hs @@ -8,7 +8,6 @@ import Control.Monad.Except import Data.Maybe ( catMaybes ) - import Environment (D (..), TcMonad) import Environment qualified as Env import Equal qualified @@ -28,7 +27,7 @@ import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = case t of +inferType a = case a of -- i-var (Var x) -> do decl <- Env.lookupTy x -- make sure the variable is accessible @@ -46,30 +45,30 @@ inferType t = case t of return TyType -- i-app - (App t1 t2) -> do - ty1 <- inferType t1 + (App a b) -> do + ty1 <- inferType a let ensurePi = Equal.ensurePi (ep1, tyA, bnd) <- ensurePi ty1 - unless (ep1 == argEp t2) $ Env.err + unless (ep1 == argEp b) $ Env.err [DS "In application, expected", DD ep1, DS "argument but found", - DD t2, DS "instead." ] + DD b, DS "instead." ] -- if the argument is Irrelevant, resurrect the context (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ - checkType (unArg t2) tyA - return (Unbound.instantiate bnd [unArg t2]) + checkType (unArg b) tyA + return (Unbound.instantiate bnd [unArg b]) -- i-ann - (Ann tm ty) -> do - tcType ty - checkType tm ty - return ty + (Ann a tyA) -> do + tcType tyA + checkType a tyA + return tyA -- Practicalities -- remember the current position in the type checking monad - (Pos p tm) -> - Env.extendSourceLocation p tm $ inferType tm + (Pos p a) -> + Env.extendSourceLocation p a $ inferType a -- Extensions to the core language -- i-unit @@ -80,19 +79,14 @@ inferType t = case t of TyBool -> return TyType -- i-true/false - (LitBool b) -> return TyBool + (LitBool _) -> return TyBool -- i-if - (If t1 t2 t3) -> do - checkType t1 TyBool - ty <- inferType t2 - checkType t3 ty - return ty - -- i-eq - (TyEq a b) -> do - aTy <- inferType a - checkType b aTy - return TyType + (If a b1 b2) -> do + checkType a TyBool + tyA <- inferType b1 + checkType b2 tyA + return tyA -- i-sigma (TySigma tyA bnd) -> do @@ -100,12 +94,17 @@ inferType t = case t of tcType tyA Env.extendCtx (mkDecl x tyA) $ tcType tyB return TyType + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType -- cannot synthesize the type of the term - tm -> - Env.err [DS "Must have a type for", DD tm] + _ -> + Env.err [DS "Must have a type annotation for", DD a] ------------------------------------------------------------------------- @@ -117,52 +116,77 @@ tcType tm = Env.withStage Irr $ checkType tm TyType ------------------------------------------------------------------------- -- | Check that the given term has the expected type checkType :: Term -> Type -> TcMonad () -checkType tm ty' = do - ty <- Equal.whnf ty' +checkType tm ty = do + ty' <- Equal.whnf ty case tm of -- c-lam: check the type of a function - (Lam ep1 bnd) -> case ty of + (Lam ep1 bnd) -> case ty' of (TyPi ep2 tyA bnd2) -> do -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 + (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 -- epsilons should match up unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, DS "but found", DD ep1, DS "instead."] -- check the type of the body of the lambda expression Env.extendCtx (Decl (TypeDecl x ep1 tyA)) (checkType body tyB) - _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty'] -- Practicalities - (Pos p tm) -> - Env.extendSourceLocation p tm $ checkType tm ty + (Pos p a) -> + Env.extendSourceLocation p a $ checkType a ty' TrustMe -> return () PrintMe -> do gamma <- Env.getLocalCtx Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] + DS "\nGoal:", DD ty'] -- Extensions to the core language -- c-if - (If t1 t2 t3) -> do - checkType t1 TyBool - dtrue <- Equal.unify [] t1 (LitBool True) - dfalse <- Equal.unify [] t1 (LitBool False) - Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - + (If a b1 b2) -> do + checkType a TyBool + dtrue <- Equal.unify [] a (LitBool True) + dfalse <- Equal.unify [] a (LitBool False) + Env.extendCtxs dtrue $ checkType b1 ty' + Env.extendCtxs dfalse $ checkType b2 ty' + -- c-prod + (Prod a b) -> do + case ty' of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + + -- c-letpair + (LetPair p bnd) -> do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body tyA + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + -- c-let - (Let rhs bnd) -> do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - Env.extendCtxs [mkDecl x aty, Def x rhs] $ - checkType body ty - + (Let a bnd) -> do + (x, b) <- Unbound.unbind bnd + tyA <- inferType a + Env.extendCtxs [mkDecl x tyA, Def x a] $ + checkType b ty' -- c-refl - Refl -> case ty of + Refl -> case ty' of (TyEq a b) -> Equal.equate a b - _ -> Env.err [DS "Refl annotated with", DD ty] + _ -> Env.err [DS "Refl annotated with invalid type", DD ty'] -- c-subst (Subst a b) -> do -- infer the type of the proof 'b' @@ -173,7 +197,7 @@ checkType tm ty' = do edecl <- Equal.unify [] m n -- if proof is a variable, add a definition to the context pdecl <- Equal.unify [] b Refl - Env.extendCtxs (edecl ++ pdecl) $ checkType a ty + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty' -- c-contra (Contra p) -> do ty' <- inferType p @@ -195,40 +219,13 @@ checkType tm ty' = do DS "are contradictory" ] - -- c-prod - (Prod a b) -> do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - - -- c-letpair - (LetPair p bnd) -> do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ - checkType body ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] - -- c-infer - tm -> do - ty' <- inferType tm - Equal.equate ty' ty + a -> do + tyA <- inferType a + Equal.equate tyA ty'