Commit cf6725f6 authored by POTTIER Francois's avatar POTTIER Francois

Added [ParallelRed].

parent 578db004
......@@ -2,6 +2,7 @@ open Printf
open AlphaLib
open Term
open TermGenerator
open ParallelRed
module T =
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. *)
| t ->
TLambda (x, t)
| 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)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment