%{

== Session 4: Type Preservation Answer ==

=== Syntax ===

}%

tp : type.  %name tp T.

nat	: tp.
arr	: tp -> tp -> tp.


exp : type.  %name exp E.

z	: exp.
fun	: tp -> tp -> (exp -> exp -> exp) -> exp.
app	: exp -> exp -> exp.

%{ 
TASK 1:
}%

s	: exp -> exp.
ifz	: exp -> exp -> (exp -> exp) -> exp.

%{

===  Static Semantics ===

}%

of : exp -> tp -> type.  %name of Dof.

of/z		: of z nat.

of/fun		: of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2)
		   <- ({f} of f (arr T1 T2)
			 -> {x} of x T1
			 -> of (E f x) T2).

of/app		: of (app E1 E2) T'
		   <- of E1 (arr T T')
		   <- of E2 T.

%{ 
TASK 2:
}%
of/s		: of (s E) nat
		   <- of E nat.

of/ifz		: of (ifz E E1 ([x] E2 x)) T
		   <- of E nat
		   <- of E1 T
		   <- ({x} of x nat -> of (E2 x) T).



%{  

=== Dynamic Semantics ===

}%

value : exp -> type.  %name value Dval.

value/z		: value z.

value/s		: value (s E)
		   <- value E.

value/fun	: value (fun _ _ _).


step : exp -> exp -> type.  %name step Dstep.

step/app/fun	: step (app E1 E2) (app E1' E2)
		   <- step E1 E1'.

step/app/arg	: step (app E1 E2) (app E1 E2')
		   <- value E1
		   <- step E2 E2'.

step/app/beta-v	: step (app (fun T1 T2 ([f] [x] E1 f x)) E2) (E1 (fun T1 T2 ([f] [x] E1 f x)) E2)
		   <- value E2.

%{ 
TASK 3:
}%
step/s		: step (s E) (s E')
		   <- step E E'.

step/ifz/arg	: step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))
		   <- step E E'.

step/ifz/z	: step (ifz z E1 ([x] E2 x)) E1.

step/ifz/s	: step (ifz (s E) E1 ([x] E2 x)) (E2 E)
		   <- value E.



%{ 

=== Preservation ===

}%


preservation : of E T
		-> step E E' 
%%
		-> of E' T
		-> type.
%mode preservation +Dof +Dstep -Dof'.

-	: preservation
	   (of/app
	      (DofE2 : of E2 T)
	      (DofE1 : of E1 (arr T T')))
	   (step/app/fun
	      (Dstep : step E1 E1')
	      : step (app E1 E2) (app E1' E2))
	   %%
	   (of/app DofE2 DofE1')
	   <- preservation DofE1 Dstep (DofE1' : of E1' (arr T T')).

-	: preservation
	   (of/app
	      (DofE2 : of E2 T)
	      (DofE1 : of E1 (arr T T')))
	   (step/app/arg
	      (Dstep : step E2 E2')
	      _
	      : step (app E1 E2) (app E1 E2'))
	   %%
	   (of/app DofE2' DofE1)
	   <- preservation DofE2 Dstep (DofE2' : of E2' T).

-	: preservation
	   (of/app
	      (DofE2 : of E2 T1)
	      (of/fun
		 (DofE1 : {f} of f (arr T1 T2) -> {x} of x T1 -> of (E1 f x) T2)
		 : of (fun T1 T2 ([f] [x] E1 f x)) (arr T1 T2)))
	   (step/app/beta-v _
	      : step (app (fun T1 T2 ([f] [x] E1 f x)) E2) (E1 (fun T1 T2 ([f] [x] E1 f x)) E2))
	   %%
	   (DofE1 (fun T1 T2 ([f] [x] E1 f x)) (of/fun DofE1) E2 DofE2).


%{ 
TASK 4:
}%

-	: preservation 
	   (of/s
	      (Dof : of E nat))
	   (step/s 
	      (Dstep : step E E')
	      : step (s E) (s E'))
	   %%
	   (of/s Dof')
	   <- preservation Dof Dstep (Dof' : of E' nat).

-	: preservation
	   (of/ifz
	      (DofE2 : {x} of x nat -> of (E2 x) T)
	      (DofE1 : of E1 T)
	      (DofE : of E nat))
	   (step/ifz/arg
	      (Dstep : step E E')
	      : step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x)))
	   %%
	   (of/ifz DofE2 DofE1 DofE')
	   <- preservation DofE Dstep (DofE' : of E' nat).

-	: preservation
	   (of/ifz
	      (DofE2 : {x} of x nat -> of (E2 x) T)
	      (DofE1 : of E1 T)
	      of/z)
	   (step/ifz/z
	      : step (ifz z E1 ([x] E2 x)) E1)
	   %%
	   DofE1.

-	: preservation
	   (of/ifz
	      (DofE2 : {x} of x nat -> of (E2 x) T)
	      (DofE1 : of E1 T)
	      (of/s
		 (DofE : of E nat)))
	   (step/ifz/s _
	      : step (ifz (s E) E1 ([x] E2 x)) (E2 E))
	   %%
	   (DofE2 E DofE).

%worlds () (preservation _ _ _).
%total D (preservation _ D _).