(* This module implements call-by-name reduction *)
(* $Id: cbn.ml,v 1.8 2000/07/19 14:25:22 alamstei Exp $ *)

open Lambda

(* 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 NormalForm;;

(* thrown to indicate that a run-time error occurred.  string is a description
   of the error, and lambdaterm is the offending term.  There are currently 
   the following sources of runtime errors:

   1.  a term does not reduce, but is not a normal form.  This happens:
       a.  in MN, if M is a normal form other than an abstraction
       b.  in pij/k M, if M is a normal form other than tuple
       c.  in case M of ..., if M is a normal form other than an injection
   2.  if we try to calculate a projection of a tuple that does not exist
   3.  if we try to match an injection where there is no matching case
   4.  if there is an error in a basic function, wuch as division by 0
*)

let rec reduce_cbn_step term =

  (* first, see if a reduction of standard functions applies *)
  try 
    Stdlib.reduce_cbn term reduce_cbn_step NormalForm
  with
    Stdlib.Not_reduced ->
      match term with
    	Var(x) -> raise NormalForm
      | App(Abs(x,m),n) -> Lambda.substitute m x n 
      | App(m,n) -> 
	  begin
      	    try
      	      App((reduce_cbn_step m), n)
      	    with
	      NormalForm -> 
	    	raise (Exn.Runtimeerror("non-function in application",term))
	  end
      | Abs(x,m) -> raise NormalForm
      | Let(x,n,m) -> Lambda.substitute m x n 
      | Letrec(x,n,m) -> Lambda.substitute m x (Letrec(x,n,n))
      | Intlit(n) -> raise NormalForm
      | Boollit(b) -> raise NormalForm
      | Tuple(tuplelist) -> raise NormalForm
      | Proj(i,j,Tuple(tuplelist)) -> 
	  begin
      	    try
	      List.nth tuplelist (i-1)
      	    with
	      Failure"nth" -> 
	    	raise (Exn.Runtimeerror("projection failure",term))
	  end
      | Proj(i,j,m) -> 
	  begin
	    try
	      let m' = reduce_cbn_step m in
	      Proj(i,j,m')
	    with
	      NormalForm -> raise 
		  (Exn.Runtimeerror("non-tuple in projection",term))
	  end
      | Inj(i,j,m) -> raise NormalForm
      | Case(Inj(i,j,m),injlist) ->
	  begin
      	    try
	      let f = fun (a,b,c,d) -> a=i && b=j in 
	      let (a,b,x,d) = (List.find f injlist) in
	      substitute d x m
      	    with
	      Not_found -> raise (Exn.Runtimeerror("match failure",term))
	  end      	
      | Case(m,injlist) -> 
	  begin
	    try
	      let m' = reduce_cbn_step m in
	      Case(m',injlist)
	    with
	      NormalForm ->
	    	raise (Exn.Runtimeerror("non-injection in case distinction",term))
	  end
	    
let rec reduce_cbn term =
  try 
    reduce_cbn (reduce_cbn_step term) 
  with
    NormalForm -> term

let rec cbn_normalform term =
  match term with
    Var(x) -> true
  | Abs(x,m) -> true
  | Intlit(n) -> true
  | Boollit(b) -> true
  | Tuple(tuplelist) -> true
  | Inj(i,j,m) -> true
  | _ -> false