ParallelRed.ml 915 Bytes
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
open AlphaLib
open Term
module T = Toolbox.Make(Term)
open T

let rec red t =
  match t with
  | TVar x ->
      TVar x
  | TLambda (x, t) ->
      begin match red t with
      | TApp (u, TVar y) when Atom.equal x y && not (occurs_term x u) ->
          (* Eta-reduction. *)
          u
      | t ->
          TLambda (x, t)

      end
  | TApp (t1, t2) ->
      let t1 = red t1
      and t2 = red t2 in
      match t1 with
      | TLambda (x, u1) ->
          (* method 1: copy [u1] so as to avoid name capture *)
          (* subst_TVar_term1 (fun t2 -> t2) t2 x (copy_term u1) *)
          (* method 2: impose the invariant that our terms do not
             have shadowing; this invariant guarantees that [u1]
             does not need to be copied; instead, [t2] must be
             copied so as to maintain the invariant. *)
          subst_TVar_term1 copy_term t2 x u1
      | _ ->
          TApp (t1, t2)