%%%%%  Conversion Regularity -- IL side (Explicit Context)  %%%%%

aconverte-reg-il : aconverte G R A _ -> aofe G R A -> type.
%mode aconverte-reg-il +X1 -X2.

converte-reg-il : converte G M A _ -> ofe G M A -> type.
%mode converte-reg-il +X1 -X2.

tconverte-reg-il : tconverte G A _ -> wfe G A -> type.
%mode tconverte-reg-il +X1 -X2.

-const	: aconverte-reg-il (aconverte/const Dconv Dwf Dkof) (aofe/closed Dord (aof/const Dwf Dkof))
	   <- tconverte-context Dconv Dord.

-forall	: aconverte-reg-il (aconverte/forall Dconv) (aofe/forall Dwf)
	   <- tconverte-reg-il Dconv Dwf.

-var	: aconverte-reg-il (aconverte/var _ Dconv Dlook) (aofe/var Dwf Dlook)
	   <- tconverte-reg-il Dconv Dwf.

-vari	: aconverte-reg-il (aconverte/vari _ Dconv Dwf Dvof) (aofe/closed Dord (aof/var Dwf Dvof))
	   <- tconverte-context Dconv Dord.

-app	: aconverte-reg-il (aconverte/app Dsub DconvM DconvR) (aofe/app DwfBx Dsub DofM DofR)
	   <- aconverte-reg-il DconvR DofR
	   <- converte-reg-il DconvM DofM
	   <- aofe-reg DofR (wfe/pi DwfB _)
	   <- tsubst-e ([_] append/nil) csub/base DofM Dsub DwfB DwfBx.
	   
-pi1	: aconverte-reg-il (aconverte/pi1 Dconv) (aofe/pi1 Dof)
	   <- aconverte-reg-il Dconv Dof.

-pi2	: aconverte-reg-il (aconverte/pi2 Dconv) (aofe/pi2 Dof)
	   <- aconverte-reg-il Dconv Dof.



-at	: converte-reg-il (converte/at Dconv) (ofe/at Dof)
	   <- aconverte-reg-il Dconv Dof.

-lam	: converte-reg-il (converte/lam Dconv2 Dconv1) (ofe/lam Dof Dwf)
	   <- tconverte-reg-il Dconv1 Dwf
	   <- ({x} {d} {ex} {xt}
		 converte-reg-il (Dconv2 x d ex xt) (Dof x d)).

-pair	: converte-reg-il (converte/pair Dwf Dconv2 Dsub Dconv1) (ofe/pair Dwf Dof2 Dsub Dof1)
	   <- converte-reg-il Dconv1 Dof1
	   <- converte-reg-il Dconv2 Dof2.

-sing	: converte-reg-il (converte/sing Dconv) (ofe/sing Dof)
	   <- aconverte-reg-il Dconv Dof.



-t	: tconverte-reg-il (tconverte/t Dord) (wfe/t Dord).

-pi	: tconverte-reg-il (tconverte/pi Dconv2 Dconv1) (wfe/pi Dwf2 Dwf1)
	   <- tconverte-reg-il Dconv1 Dwf1
	   <- ({x} {d} {ex} {xt}
		 tconverte-reg-il (Dconv2 x d ex xt) (Dwf2 x d)).

-sigma	: tconverte-reg-il (tconverte/sigma Dconv2 Dconv1) (wfe/sigma Dwf2 Dwf1)
	   <- tconverte-reg-il Dconv1 Dwf1
	   <- ({x} {d} {ex} {xt}
		 tconverte-reg-il (Dconv2 x d ex xt) (Dwf2 x d)).

-sing	: tconverte-reg-il (tconverte/sing Dconv) (wfe/sing Dof)
	   <- aconverte-reg-il Dconv Dof.

%worlds (fbind | fobind | bind | ovar | tbind | evar) (aconverte-reg-il _ _) (converte-reg-il _ _) (tconverte-reg-il _ _).
%total (D1 D2 D3) (aconverte-reg-il D1 _) (converte-reg-il D2 _) (tconverte-reg-il D3 _).




%%%%%  Conversion Regularity -- IL side  %%%%%

tconvert-reg-il	: tconvert A _ -> wf A -> type.
%mode tconvert-reg-il +X1 -X2.

-	: tconvert-reg-il Dconv Dwf
	   <- tconvert-to-tconverte Dconv Dconve
	   <- tconverte-reg-il Dconve Dwfe
	   <- wfe-to-wf Dwfe Dwf.

%worlds (fbind | bind | tbind) (tconvert-reg-il _ _).
%total {} (tconvert-reg-il _ _).



convert-reg-il : convert M A _ -> of M A -> type.
%mode convert-reg-il +X1 -X2.

-	: convert-reg-il Dconv Dof
	   <- convert-to-converte Dconv Dconve
	   <- converte-reg-il Dconve Dofe
	   <- ofe-to-of Dofe Dof.

%worlds (fbind | bind | tbind | eofblock) (convert-reg-il _ _).
%total {} (convert-reg-il _ _).



aconvert-reg-il : aconvert R A _ -> aof R A -> type.
%mode aconvert-reg-il +X1 -X2.

-	: aconvert-reg-il Dconv Dof
	   <- aconvert-to-aconverte Dconv Dconve
	   <- aconverte-reg-il Dconve Dofe
	   <- aofe-to-aof Dofe Dof.

%worlds (fbind | bind | tbind) (aconvert-reg-il _ _).
%total {} (aconvert-reg-il _ _).