(* beta reduction *)
(* $Id: beta.ml,v 1.20 2000/07/02 19:26:33 alamstei Exp $ *)

open Lambda
open List

(* thrown to indicate that a term which was passed to a function with the 
   intention of it being reduced is already in normal form *)
exception CannotReduceAnf;;

(* test for normal form *)
let rec normalform term =
  match term with
    Var(x) -> true
  | App(Abs(x, p), n) -> false
  | App(m, n) -> normalform m && normalform n
  | Abs(x, m) -> normalform m
  | Let(x,m,n) -> false
  | Letrec(x,m,n) -> false
  | Intlit(n) -> true
  | Boollit(n) -> true
  | Tuple(termlist) -> List.for_all normalform termlist
  | Proj(i,j,m) -> normalform m
  | Inj(i,j,m) -> normalform m
  | Case(Inj(i,j,m),injlist) -> false
  | Case(m,injlist) -> 
      normalform m && (List.for_all (fun (i,j,x,m) -> normalform m) injlist)

(* single step reduction *) 
(* Assume that reduce_leftmost *always* reduces the term, and raise an
   exception if reduce_leftmost is applied to a normal form *)

let rec reduce_leftmost term =

  let rec reduce_first_term termlist =
    match termlist with
      hd::tl -> 
	begin
	  try
	    (reduce_leftmost hd)::tl
	  with
	    CannotReduceAnf -> 
	      hd::(reduce_first_term tl)
	end
    | [] -> raise CannotReduceAnf
  in
  
  let rec reduce_injlist injlist =
    match injlist with
      (a,b,x,m)::tl ->
	begin	
	  try 
	    (a,b,x,(reduce_leftmost m))::tl
	  with
	    CannotReduceAnf -> (a,b,x,m)::(reduce_injlist tl)
        end
    | _ -> []
  in

  match term with
    Var(x) -> raise CannotReduceAnf 
  | App(Abs(o, p), n) -> substitute p o n
  | App(m, n) -> 
      begin
	try
	  App (reduce_leftmost m, n)
	with CannotReduceAnf ->
	  App(m, reduce_leftmost n)
      end
  | Abs(x, m) -> Abs(x, reduce_leftmost m)
  | Let(x,m,n) -> substitute n x m
  | Letrec(x,n,m) -> Lambda.substitute m x (Letrec(x,n,n))
  | Intlit(n) -> raise CannotReduceAnf
  | Boollit(n) -> raise CannotReduceAnf
  | Tuple(termlist) -> Tuple(reduce_first_term termlist)
  | Proj(i,j,m) ->
      begin
	try
	  let Tuple(termlist) = m in
	  List.nth termlist (i-1)
	with
	  Failure("nth") | Match_failure(_,_,_) ->
	    Proj(i,j,(reduce_leftmost m))
      end
  | Inj(i,j,n) -> Inj(i,j,(reduce_leftmost n))
  | Case(m,injlist) -> 
      begin
      	try
	  let Inj(i,j,n) = m in
      	  let f = fun (a,b,x,p) -> a=i && b=j in
	  let (_,_,x,p) = List.find f injlist in
          substitute p x n
      	with
	  Not_found | Match_failure (_,_,_) -> 
	    begin
	      try
	      	Case((reduce_leftmost m),injlist)
	      with
	      	CannotReduceAnf -> Case(m,(reduce_injlist injlist))
	    end
      end

let rec reduce_to_nf term =
  try 
    reduce_to_nf (reduce_leftmost term) 
  with
    CannotReduceAnf -> term