structure Evaluator :> EVALUATOR =
struct
  open TermOps
  open Term

  infix 5 $
  infix 5 \
  infix 5 $$

  exception Runtime_Error
  exception Not_Implemented
  
  type state = Term.t
  datatype result =
    Fork of (state * state * (state -> state -> state))
  | Continue of (state * (state -> state))
	
  val par = false
  val letpar = true
  
  fun is_value e =
    case out e of
      Zero $ []       => true
    | Succ $ [e']     => is_value e'
    | (Lam _) $ [_]   => true
    | Pair $ [e1, e2] => (is_value e1) andalso (is_value e2)
    | Triv $ []       => true
    | (Nil _) $ []    => true
    | Cons $ [e1, e2] => (is_value e1) andalso (is_value e2)
    | True $ []       => true
    | False $ []      => true
    | _ => false

	fun id e = e
	
	fun is_final e = is_value e
	fun load t = t
	fun unload t = t
	
	fun step e = 
		case Term.out e of
			Term.$(TermOps.Succ, [e1]) => Continue (e1, fn e1' => Succ $$ [e1'])
		|   Term.$(TermOps.Ifz,[e1,e2,e3]) => if is_value e1 then
				(case out e1 of
					Zero $ [] => Continue (e2, fn e1' => e1') 
				|	Succ $ [ep] =>
					(case out e3 of
						x \ e3' => Continue (subst ep x e3', fn e1' => e1')
					|	_ => raise Runtime_Error)
				|	_ => raise Runtime_Error)
				else Continue (e1, fn e1' => Ifz $$ [e1', e2, e3])
		| 	Term.$(TermOps.Ap,[e1,e2]) => if is_value e1 then
				( case out e1 of
					(Lam _) $ [xe'] =>
						(case out xe' of
							x \ e' => Continue (subst e2 x e', fn e1' => e1') 
						| _ => raise Runtime_Error)
					| _ => raise Runtime_Error)
				else Continue (e1, fn e1' => Ap $$ [e1', e2] )
		| 	Term.$(TermOps.Fix(t), [e1]) => 
				(case out e1 of
					x \ e' => Continue (subst e x e', fn e1' => e1') 
				|	_ => raise Runtime_Error)
		|	Term.$(TermOps.Pair, [e1, e2]) => if is_value e1 then Continue (e2, fn e2' => Pair $$ [e1, e2']) 
												else Continue (e1, fn e1' => Pair $$ [e1', e2])
		|	Term.$(TermOps.ProjL, [e1]) => 
			if is_value e1 then
				(case out e1 of
					Pair $ [e1', e2] => Continue (e1', fn x => x) 
				|	_ => raise Runtime_Error)
			else Continue (e1, fn e1' => ProjL $$ [e1']) 
		|	Term.$(TermOps.ProjR, [e1]) => 
			if is_value e1 then
				(case out e1 of
					Pair $ [e1', e2] => Continue (e2, fn x => x) 
				|	_ => raise Runtime_Error)
			else Continue (e1, fn e1' => ProjR $$ [e1']) 
		|	Term.$(TermOps.Let, [e1,e2,e3]) =>
				if is_value e1 then
					if is_value e2 then
						( case out e3 of
							x1 \ e3' =>
								(case out e3' of
									x2 \ e3'' => Continue (subst e2 x2 (subst e1 x1 e3''), fn x => x) 
									| _ => raise Runtime_Error)  
							| _ => raise Runtime_Error)  
					else Continue (e2, fn e2' => Let $$ [e1, e2', e3])
				else if is_value e2 then
						Continue (e1, fn e1' => Let $$ [e1', e2, e3])
					else Fork (e1, e2, fn e1' =>  fn e2' =>  Let $$ [e1', e2', e3])
		|	Term.$(TermOps.Cons, [e1, e2]) =>
				if is_value e1 then Continue (e2, fn e2' => Cons $$ [e1, e2'])
				else Continue (e1, fn e1' => Cons $$ [e1', e2])
		|	Term.$(TermOps.ListRec, [e1, e2, e3]) =>
			if is_value e1 then
				(case out e1 of
					Nil _ $ [] => Continue (e2, fn e1' => e1') (*EListRecNil*)
				|	Cons $ [h, t] => 
					(case out e3 of
						w \ e3' =>
							(case out e3' of
								y \ e3'' =>
								(case out e3'' of
									z \ e3''' => 
										let
											(*
											val e1' = subst e1 w h
											val e1'' = subst e1' y t
											val e1''' = subst e1'' z (ListRec $$ [t, e2, e3])
											*)
											val e1' = subst h w e3
											val e1'' = subst t y e1'
											val e1''' = subst (ListRec $$ [t, e2, e3]) z e1''
										in
											Continue(e1''', fn x => x)
										end
									|	_ => raise Runtime_Error)
							|	_ => raise Runtime_Error)
					|	_ => raise Runtime_Error)
				|	_ => raise Runtime_Error)
			else Continue (e1, fn e1' => ListRec $$ [e1', e2, e3]) (*EListRecCong*)
		|	Term.$(TermOps.IfElse, [e1, e2, e3]) =>
			if is_value e1 then
				(case out e1 of
					True $ [] => Continue (e2, fn x => x)
					| False $ [] => Continue (e3, fn x => x) 
					|	_ => raise Runtime_Error)
			else Continue (e1, fn e1' => IfElse $$ [e1', e2, e3])
		|	_ => raise Runtime_Error
end