Module Projection

$\displaystyle \mathsf{proj}(M, \mathsf{con} \; x :: \kappa \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle \kappa$
$\displaystyle \mathsf{proj}(M, \mathsf{con} \; x :: \kappa = c \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle (\kappa, c)$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle \mathsf{Type}^{\mathsf{len}(\overline{y})} \to \mathsf{Type}$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle (\mathsf{Type}^{\mathsf{len}(\overline{y})} \to \mathsf{Type}, M'... ...trm{ (where $\Gamma \vdash M' : \mathsf{sig} \; \overline{s'} \; \mathsf{end}$}$
		$\displaystyle \textrm{and $\mathsf{proj}(M', \overline{s'}, \mathsf{datatype} \; z) = (\overline{y}, \overline{dc})$)}$
$\displaystyle \mathsf{proj}(M, \mathsf{class} \; x :: \kappa \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle \kappa \to \mathsf{Type}$
$\displaystyle \mathsf{proj}(M, \mathsf{class} \; x :: \kappa = c \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle (\kappa \to \mathsf{Type}, c)$

$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mathsf{datatype} \; x)$	$\displaystyle =$	$\displaystyle (\overline{y}, \overline{dc})$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z \; \overline{s}, \mathsf{con} \; x)$	$\displaystyle =$	$\displaystyle \mathsf{proj}(M', \overline{s'}, \mathsf{datatype} \; z) \textrm{ (where $\Gamma \vdash M' : \mathsf{sig} \; \overline{s'} \; \mathsf{end}$)}$

$\displaystyle \mathsf{proj}(M, \mathsf{val} \; x : \tau \; \overline{s}, \mathsf{val} \; x)$	$\displaystyle =$	$\displaystyle \tau$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mathsf{val} \; X)$	$\displaystyle =$	$\displaystyle \overline{y ::: \mathsf{Type}} \to M.x \; \overline y \textrm{ (where $X \in \overline{dc}$)}$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mathsf{val} \; X)$	$\displaystyle =$	$\displaystyle \overline{y ::: \mathsf{Type}} \to \tau \to M.x \; \overline y \textrm{ (where $X \; \mathsf{of} \; \tau \in \overline{dc}$)}$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z, \mathsf{val} \; X)$	$\displaystyle =$	$\displaystyle \overline{y ::: \mathsf{Type}} \to M.x \; \overline y \textrm{ (where $\Gamma \vdash M' : \mathsf{sig} \; \overline{s'} \; \mathsf{end}$}$
		$\displaystyle \textrm{and $\mathsf{proj}(M', \overline{s'}, \mathsf{datatype} \; z = (\overline{y}, \overline{dc})$\ and $X \in \overline{dc}$)}$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z, \mathsf{val} \; X)$	$\displaystyle =$	$\displaystyle \overline{y ::: \mathsf{Type}} \to \tau \to M.x \; \overline y \textrm{ (where $\Gamma \vdash M' : \mathsf{sig} \; \overline{s'} \; \mathsf{end}$}$
		$\displaystyle \textrm{and $\mathsf{proj}(M', \overline{s'}, \mathsf{datatype} \... ...verline{y}, \overline{dc})$\ and $X \; \mathsf{of} \; \tau \in \overline{dc}$)}$

$\displaystyle \mathsf{proj}(M, \mathsf{structure} \; X : S \; \overline{s}, \mathsf{structure} \; X)$	$\displaystyle =$	$\displaystyle S$

$\displaystyle \mathsf{proj}(M, \mathsf{signature} \; X = S \; \overline{s}, \mathsf{signature} \; X)$	$\displaystyle =$	$\displaystyle S$

$\displaystyle \mathsf{proj}(M, \mathsf{con} \; x :: \kappa \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [x \mapsto M.x]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{con} \; x :: \kappa = c \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [x \mapsto M.x]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [x \mapsto M.x]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [x \mapsto M.x]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{val} \; x : \tau \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle \mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{structure} \; X : S \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [X \mapsto M.X]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{signature} \; X = S \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [X \mapsto M.X]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{include} \; S \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle \mathsf{proj}(M, \overline{s'} \; \overline{s}, V) \textrm{ (where $\Gamma \vdash S \equiv \mathsf{sig} \; \overline{s'} \; \mathsf{end}$)}$
$\displaystyle \mathsf{proj}(M, \mathsf{constraint} \; c_1 \sim c_2 \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle \mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{class} \; x :: \kappa \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [x \mapsto M.x]\mathsf{proj}(M, \overline{s}, V)$
$\displaystyle \mathsf{proj}(M, \mathsf{class} \; x :: \kappa = c \; \overline{s}, V)$	$\displaystyle =$	$\displaystyle [x \mapsto M.x]\mathsf{proj}(M, \overline{s}, V)$