%{

== Syntax ==

}%

tp : type.				%name tp T.
num : tp.
arr : tp -> tp -> tp.

exp : type.				%name exp E.
fn : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
z : exp.
s : exp -> exp.

%{
==== Exercise: constant for ifz ====
}%

%% The syntax '% .' (without the space)
%% causes Twelf to stop processing the file at this point
%% remove once you have completed the exercise
%.

%{

== Static semantics ==

}%

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

of/z : of z num.

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

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

%{ 
==== Exercise: typing rules for s and ifz ====
}%










%block of_block : some {T:tp} block {x:exp}{dx: of x T}.
%worlds (of_block) (of _ _).

%{

== Dynamic semantics ==

=== value judgement ===


}%

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

value/fn : value (fn T ([x] E x)).
%{ 
==== Exercise: value rules for z and s ====
}%







%{

=== step judgement ===

}%

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

step/app/fn : 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 : step (app (fn T ([x] E x)) E2) (E E2)
		 <- value E2.

%{ 
==== Exercise: step rules for s and ifz ====
}%






%{ 

== Progress theorem ==

=== Sum type for the result ===

}%

val-or-step : exp -> type.        %name val-or-step Dvos.

vos/value : val-or-step E
	     <- value E.
vos/step  : val-or-step E
	     <- step E E'.

%{

=== Lemmas ===

}%

prog/app : of E1 (arr T' T) 
	    -> val-or-step E1
	    -> val-or-step E2
	    -> val-or-step (app E1 E2)
	    -> type.
%mode prog/app +Dof +Dvos1 +Dvos2 -Dvos.

- : prog/app 
     _ 
     (vos/step (Dstep1 : step E1 E1'))
     _
     (vos/step (step/app/fn Dstep1)).

- : prog/app
     _
     (vos/value (Dval1 : value E1))
     (vos/step (Dstep2 : step E2 E2'))
     (vos/step (step/app/arg Dstep2 Dval1)).

- : prog/app
     (of/fn _ : of (fn T ([x] E' x)) (arr T T'))
     (vos/value (Dval1 : value (fn T ([x] E' x))))
     (vos/value (Dval2 : value E2))
     (vos/step (step/app/beta Dval2)).

%worlds () (prog/app _ _ _ _).
%total {} (prog/app _ _ _ _).

%{

==== Exercise: lemma for s ====

}%








%{

==== Exercise: lemma for ifz ====

}%








%{

=== Main theorem ===

}%

prog : of E T -> val-or-step E -> type.
%mode prog +Dof -Dvos.

- : prog (of/z : of z num) (vos/value (value/z : value z)).

- : prog (of/fn _) (vos/value value/fn).

- : prog (of/app 
	    (D2 : of E2 T') 
	    (D1 : of E1 (arr T' T)))
     DvosApp
     <- prog D1 (Dvos1 : val-or-step E1)
     <- prog D2 (Dvos2 : val-or-step E2)
     <- prog/app D1 Dvos1 Dvos2 DvosApp.

%{ 

==== Exercise: cases for s and ifz ====

}%








%worlds () (prog _ _).
%total Dof (prog Dof _).