Module voile::check::unify

Meta variable solving, term (definitional) equality comparison. $$ \Gamma \vdash A \simeq B $$

Functions

check_solution
solve_with	Solve a meta with a specific value.
unify	Try to unify two well-typed terms, using a conversion check algorithm. This may lead to meta variable resolution. $$ \newcommand{\Gvdash}[0]{\Gamma \vdash} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \newcommand{\recordext}[2]{\record{#1 \mid #2}} \newcommand{\clabVal}[0]{\delta} \newcommand{\recExt}[1]{\mid #1} \newcommand{\variantext}[2]{\variant{#1 \mid #2}} \cfrac{ \Gvdash \cA_0 \simeq \cA_1 \quad \Gvdash \cA_1 \simeq \cA_2 }{ \Gvdash \cA_0 \simeq \cA_2 } \quad \cfrac{}{\Gvdash \cA \simeq \cA} \\ \space \\ \cfrac{}{ \Gvdash \{\} \simeq \{\} } \quad \cfrac{\Gvdash \alpha \simeq \beta}{ \Gvdash n\ \alpha \simeq n\ \beta \quad \cfrac{\Gvdash \{ \clabVal_0 \} \simeq \{ \clabVal_1 \}}{ \Gvdash \{ n\ = \alpha, \clabVal_0 \} \simeq \{ n\ = \beta, \clabVal_1 \} } } $$
unify_case_split
unify_closure	Beta-rule in unify. $$ \newcommand{\xx}[0]{\texttt{x}} \newcommand{\Gvdash}[0]{\Gamma \vdash} \cfrac{}{ \Gvdash t \simeq \lambda \xx. t \xx \quad \Gvdash \lambda \langle \rangle \simeq \lambda \langle \rangle } $$
unify_meta_with
unify_neutral	Unify two neutral terms. $$ \newcommand{\casevS}[2]{\textbf{split}\ #1\ (#2)} \newcommand{\caseTr}[0]{\text{ct}} \newcommand{\clabVal}[0]{\delta} \newcommand{\caseextS}[2]{\textbf{split}\ (#1)\ \textbf{or}\ #2} \newcommand{\Gvdash}[0]{\Gamma \vdash} \newcommand{\recExt}[1]{\mid #1} \cfrac{ \Gvdash [k_0] \simeq [k_1] }{ \Gvdash [k_0 .n] \simeq [k_1 .n] \quad \cfrac{\Gvdash \{ \clabVal_0 \} \simeq \{ \clabVal_1 \}}{ \Gvdash [\{ \clabVal_0 \recExt{k_0} \}] \simeq [\{ \clabVal_1 \recExt{k_1} \}] } \quad } \\ \space \\ \cfrac{ \Gvdash \lambda c_0 \simeq \lambda c_1 \quad \Gvdash \lambda \langle \caseTr_0 \rangle \simeq \lambda \langle \caseTr_1 \rangle }{ \Gvdash \lambda \langle n\ c_0, \caseTr_0 \rangle \simeq \lambda \langle n\ c_1, \caseTr_1 \rangle } \\ \space \\ \cfrac{ \Gvdash [k_0] \simeq [k_1] \quad \Gvdash \lambda \langle \caseTr_0 \rangle \simeq \lambda \langle \caseTr_1 \rangle }{ \Gvdash [\caseextS{\caseTr_0}{k_0}] \simeq [\caseextS{\caseTr_1}{k_1}] \quad \Gvdash [\casevS{k_0}{\caseTr_0}] \simeq [\casevS{k_1}{\caseTr_1}] } $$
unify_neutral_variants
unify_partial_variants
unify_variants	Unify two row-polymorphic types. $$ \newcommand{\Gvdash}[0]{\Gamma \vdash} \newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4} \newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}} \newcommand{\ty}[0]{\tau} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \newcommand{\ctyLab}[0]{\gamma} \newcommand{\clabVal}[0]{\delta} \newcommand{\variant}[1]{\textbf{Sum}\ \{ #1 \}} \newcommand{\record}[1]{\textbf{Rec}\ \{ #1 \}} \cfrac{ \Gtyck{A_0}{\ty}{\cA_0} \quad \Gtyck{A_1}{\ty}{\cA_1} \quad \Gvdash \cA_0 \simeq \cA_1 \quad (n : \cA_0) \notin \ctyLab_0 \quad (n : \cA_1) \notin \ctyLab_1 }{ \cfrac{ \Gvdash \record{\ctyLab_0} \simeq \record{\ctyLab_1} }{ \Gvdash \record{n : \cA_0, \ctyLab_0} \simeq \record{n : \cA_1, \ctyLab_1} } \quad \cfrac{ \Gvdash \variant{\ctyLab_0} \simeq \variant{\ctyLab_1} }{ \Gvdash \variant{n : \cA_0, \ctyLab_0} \simeq \variant{n : \cA_1, \ctyLab_1} } } $$