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