@@ -1108,9 +1108,50 @@ natToBin' (S (j + j)) odd = True :: natToBin j
1108\useverb{natToBinwp}
1108\useverb{natToBinwp}
1110\noindent
1110\noindent
1111−Elaboration of \texttt{with} builds the type declaration and auxiliary function
1111+Additionally, the elaborator abstracts over the term being analysed in the type
1112−automatically:
1112+of the generated auxiliary definition\footnote{This is sometimes referred to
1113+as ``magic \texttt{with}''.} and reorders the arguments as required.
1116+\begin{SaveVerbatim}{magicwith}
1120+ftest : (n : Nat) -> so (f n) -> Nat
1121+ftest n x with (f n)
1129+Here, we may require the knowledge that \texttt{f n} is \texttt{True} or
1130+\texttt{False} in the appropriate case. The elaborator abstracts over
1131+\texttt{f n} in the auxiliary definition, specialising the type of
1132+\texttt{x} in each case:
1134+\begin{SaveVerbatim}{magicwithaux}
1136+ftest : (n : Nat) -> so (f n) -> Nat
1137+ftest n x = ftest' n (f n) x
1139+ftest' : (n : Nat) -> (p : Bool) -> so p -> Nat
1140+ftest' n True x = ...
1141+ftest' n False x = ...
1144+\useverb{magicwithaux}
1147+Elaboration of \texttt{with} builds the type declaration and auxiliary function
1148+automatically. It checks the left hand side, resulting in a set of patterns
1149+$\tp$, then splits these patterns into those necessary to type
1150+$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using
1151+$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over
1152+the matched expression $\ve$ in the types of $\tp_n$.
1153+$\MO{Abstract}\:\ve\:\vw\:\vp$ simply replaces any occurrence of $\vw$ in
1154+$\vp$ with the name $\ve$.
@@ -1123,17 +1164,18 @@ automatically:
1123\MO{NewTerm}\:\TC{Infer};\;
1164\MO{NewTerm}\:\TC{Infer};\;
1124\ttinterp{\DC{MkInfer}\:\_\:\ve}\\
1165\ttinterp{\DC{MkInfer}\:\_\:\ve}\\
1125\DC{MkInfer}\:\vW\:\vw'\gets\MO{Term}\\
1166\DC{MkInfer}\:\vW\:\vw'\gets\MO{Term}\\
1167+(\tp_w,\tp_n)\:\gets\:\MO{SplitContext}\:\vW\:\tp\\
1126−\MO{TTDecl}\:(\vx'\Hab\tp\to\vW\to\vT)\\
1168+\MO{TTDecl}\:(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\:\ve\:\vw'\:\tp_{n}\to\vT)\\
1127−\tc'\gets\vec{\MO{MatchWith}}\:\tp\:(\vx\:\ttt)\:\vec{\VV{pclause}}\\
1169+\tc'\gets\vec{\MO{MatchWith}}\:\tp\:\ttt\:\vec{\VV{pclause}}\\
1128\vec{\MO{Elab}}\:\tc'\\
1170\vec{\MO{Elab}}\:\tc'\\
1129−\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp\:\vw')
1171+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp_{w}\:\vw'\:\tp_{n})
1131\medskip\\
1173\medskip\\
1132−\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
1174+\MO{MatchWith}\:\tp_w\:\tp_n\:\ttt\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
1133\hg\hg\edo{
1175\hg\hg\edo{
1134\tp'\gets\vec{\MO{Match}}\:\tw\:\ttt\\
1176\tp'\gets\vec{\MO{Match}}\:\tw\:\ttt\\
1135−\MO{CheckComplete}\:\tp\:\tp'\\
1177+(\tp'_w,\tp'_n)\:\gets\:\MO{SplitPats}\:\tp_w\:\tp_n\:\tp'\\
1136−\RW{return}\:(\vx'\:\tp'\:\ve\:\VV{rhs})
1178+\RW{return}\:(\vx'\:\tp'_w\:\ve\:\tp'_{n}\:\VV{rhs})
@@ -1154,10 +1196,8 @@ The right hand side, $\VV{rhs}$, may either return a value directly, containing
1154remains unchanged.
1196remains unchanged.
1155$\MO{Match}\:\vw\:\vt$ returns a list of pattern bindings containing
1197$\MO{Match}\:\vw\:\vt$ returns a list of pattern bindings containing
1156the variables in $\vt$ and their matches in $\vw$.
1198the variables in $\vt$ and their matches in $\vw$.
1157−If the \texttt{with} block is well-formed, then
1199+The resulting matches are split, using $\MO{SplitPats}$, into matches for those
1158−the resulting set of patterns $\tp'$ contains exactly the same pattern variables
1200+variables necessary to type $\vW$ and the rest, as before.
1159−as $\tp$, which is verified by $\MO{CheckComplete}$.
1162\subsubsection{Elaborating Class and Instance Declarations}
1202\subsubsection{Elaborating Class and Instance Declarations}