-- ======================= -- Several program transformations for the LR-calculus -- ======================= -- -- -- -- T,a rules -- {lbeta} T[app (\X.S) R] ==> T[letrec X=R in S] where (R,\X.HOLE) {cpT-in} T[letrec X1 = \X.S; E in T1[var X1]] ==> T[letrec X1 = \X.S; E in T1[\X.S]] where (\X.S, T1) ,(var X1,T1) ,(S,T1) {cpd-in} T[letrec X1 = \X.S; E in C1[\Y.T2[var X1]]] ==> T[letrec X1 = \X.S; E in C1[\Y.T2[\X.S]]] where (\X.S, C1[\Y.T2]) ,(var X1,C1[\Y.T2]) ,(S,C1[\Y.T2]) {cpT-e,1} T[letrec X1 = \X.S; Y = T1[var X1];E in R] ==> T[letrec X1 = \X.S; Y = T1[\X.S];E in R] -- note that varchains are not included where (\X.S, T1) ,(var X1,T1) ,(S,T1) {cpd-e,1} T[letrec X1 = \X.S; Y = C1[\Z.T2[var X1]];E in R] ==> T[letrec X1 = \X.S; Y = C1[\Z.T2[\X.S]];E in R] -- note that varchains are not included where (\X.S, C1[\Z.T2]) ,(var X1,C1[\Z.T2]) ,(S,C1[\Z.T2]) {llet-in} T[letrec E1 in letrec E2 in S] ==> T[letrec E1;E2 in S] where E1/={} , E2/={} , [E1,letrec E2 in HOLE] {llet-e} T[letrec E1; X=letrec E2 in S1 in R] ==> T[letrec E1; E2; X=S1 in R] where E2/={} , [E1,letrec E2 in HOLE] , (R,letrec E2 in HOLE) {lapp} T[app (letrec E in R) S] ==> T[letrec E in (app R S)] where E/={} ,(S, letrec E in HOLE) {cpT-e,2} T[letrec X1 = \X.S; EE^A[Xn,T1[var X1]]; E in R] ==> T[letrec X1 = \X.S; EE^A[Xn,T1[\X.S]]; E in R] where (S,T1) ,(\X.S,T1) ,(var X1,T1) {cpd-e,2} T[letrec X1 = \X.S; EE^A[Xn,C1[\Z.T2[var X1]]]; E in R] ==> T[letrec X1 = \X.S; EE^A[Xn,C1[\Z.T2[\X.S]]]; E in R] where (S,C1[\Z.T2]) ,(\X.S,C1[\Z.T2]) ,(var X1,C1[\Z.T2]) {caselist-c,1} T[caselist[1] (nil[]) SNIL X.XS.SCONS] ==> T[SNIL] where (var X,dummylist3[] XS.HOLE) ,(var XS,dummylist3[] X.HOLE) {caselist-c,2} T[caselist (cons[] R RS) SNIL X.XS.SCONS] ==> T[letrec X=R;XS=RS in SCONS] where (R, (dummylist1[] X.XS.HOLE)) ,(RS, (dummylist2[] X.XS.HOLE)) ,(var X,dummylist3[] XS.HOLE) ,(var XS,dummylist3[] X.HOLE) {casebool-c,1} T[casebool[1] (false[]) SFALSE STRUE] ==> T[SFALSE] {casebool-c,2} T[casebool[1] (true[]) SFALSE STRUE] ==> T[STRUE] {casepair-c,1} T[casepair (pair[] R1 R2) X1.X2.S] ==> T[letrec X1=R1;X2=R2 in S] where (R1, (dummypair1[] X1.X2.HOLE)) ,(R2, (dummypair1[] X1.X2.HOLE)) ,(var X1,dummylist3[] X2.HOLE) ,(var X2,dummylist3[] X1.HOLE) {seq-c,1} T[seq (\X.R) S] ==> T[S] {seq-c,2} T[seq (nil) S] ==> T[S] {seq-c,3} T[seq (cons R1 R2) S] ==> T[S] {seq-c,4} T[seq (true) S] ==> T[S] {seq-c,5} T[seq (false) S] ==> T[S] {seq-c,6} T[seq (pair[] R1 R2) S] ==> T[S] {lcaselist} T[caselist (letrec E in R) S1 X.XS.S2] ==> T[letrec E in (caselist R S1 X.XS.S2)] where E/={} , (S1, letrec E in HOLE) , ((dummylistwww[] X.XS.S2), letrec E in HOLE) ,(var X,dummylist3[] XS.HOLE) ,(var XS,dummylist3[] X.HOLE) {lcasepair} T[casepair (letrec E in R) X1.X2.S] ==> T[letrec E in (casepair R X1.X2.S)] where E/={} , (S1, letrec E in HOLE) , ((dummypair3[] X1.X2.S), letrec E in HOLE) ,(var X1,dummylist3[] X2.HOLE) ,(var X2,dummylist3[] X1.HOLE) {lcasebool} T[casebool (letrec E in R) SFALSE STRUE] ==> T[letrec E in (casebool R SFALSE STRUE)] where E/={} , (SFALSE, letrec E in HOLE) , (STRUE, letrec E in HOLE) {lseq} T[seq (letrec E in R) S] ==> T[letrec E in (seq R S)] where E/={} , (S, letrec E in HOLE) {cpx-in,1} T[letrec X = (var Y); E in C[var X]] ==> T[letrec X = (var Y); E in C[(var Y)]] where (var X, C), (var Y, C) {cpx-e,1} T[letrec X = (var Y); Z = C[var X]; E in S] ==> T[letrec X = (var Y); Z = C[var Y]; E in S] where (var X, C), (var Y, C) -- overlaps already covered by T-cpx-e but inserted for closing diagrams: {cpx-e,2} T[letrec X = (var Y); EE^A[Z,C[var X]]; E in S] ==> T[letrec X = (var Y); EE^A[Z,C[var Y]]; E in S] where (var X, C), (var Y, C) {xch,1} T[letrec X = (var Y); Y = S1; E in S2] ==> T[letrec X = S1; Y = (var X); E in S2] {cpcx-in,1} T[letrec X = nil; E in C[var X]] ==> T[letrec X = nil; E in C[nil]] where (var X, C) {cpcx-in,2} T[letrec X = (cons R1 R2); E in C[var X]] ==> T[letrec X = (cons (var Z) (var ZS)); Z = R1; ZS = R2; E in C[(cons (var Z) (var ZS))]] where (var X, C) ,(var Z, T[letrec X = dummy3[]; ZS = dummy3[]; E in HOLE]) ,(var ZS, T[letrec X = dummy3[]; Z = dummy3[]; E in HOLE]) ,(R1, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,(R2, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,[E, letrec Z=dummy3[]; ZS=dummy3[] in HOLE] ,(C[var X], letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,((cons (var Z) (var ZS)),C) {cpcx-in,3} T[letrec X = false; E in C[var X]] ==> T[letrec X = false; E in C[false]] where (var X, C) {cpcx-in,4} T[letrec X = true; E in C[var X]] ==> T[letrec X = true; E in C[true]] where (var X, C) {cpcx-in,5} T[letrec X = (pair[] R1 R2); E in C[var X]] ==> T[letrec X = (pair[] (var Z) (var ZS)); Z = R1; ZS = R2; E in C[(pair[] (var Z) (var ZS))]] where (var X, C) ,(var Z, T[letrec X = dummy3[]; ZS = dummy3[]; E in HOLE]) ,(var ZS, T[letrec X = dummy3[]; Z = dummy3[]; E in HOLE]) ,(R1, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,(R2, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,[E, letrec Z=dummy3[]; ZS=dummy3[] in HOLE] ,((pair[] (var Z) (var ZS)),C) ,(C[var X], letrec Z=dummy3[]; ZS=dummy3[] in HOLE) {cpcx-e,1} T[letrec X = nil; Y=C[var X]; E in S] ==> T[letrec X = nil; Y=C[nil]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) {cpcx-e,2} T[letrec X = (cons R1 R2); Y=C[var X];E in S] ==> T[letrec X = (cons (var Z) (var ZS)); Z = R1; ZS = R2; Y=C[(cons (var Z) (var ZS))]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) ,(var Y, letrec X=dummy3[] in HOLE) ,(var Z, T[letrec X = dummy3[]; ZS = dummy3[]; Y=dummy3[]; E in HOLE]) ,(var ZS, T[letrec X = dummy3[]; Z = dummy3[]; Y=dummy3[]; E in HOLE]) ,(T[letrec X = (cons R1 R2); Y=C[var X];E in S], letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,((cons (var Z) (var ZS)),C) {cpcx-e,3} T[letrec X = false; Y=C[var X]; E in S] ==> T[letrec X = false; Y=C[false]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) {cpcx-e,4} T[letrec X = true; Y=C[var X]; E in S] ==> T[letrec X = true; Y=C[true]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) {cpcx-e,5} T[letrec X = (pair[] R1 R2); Y=C[var X];E in S] ==> T[letrec X = (pair[] (var Z) (var ZS)); Z = R1; ZS = R2; Y=C[(pair[] (var Z) (var ZS))]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) ,(var Y, letrec X=dummy3[] in HOLE) ,(var Z, T[letrec X = dummy3[]; ZS = dummy3[]; Y=dummy3[]; E in HOLE]) ,(var ZS, T[letrec X = dummy3[]; Z = dummy3[]; Y=dummy3[]; E in HOLE]) ,(T[letrec X = (pair[] R1 R2); Y=C[var X];E in S], letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,((pair[] (var Z) (var ZS)),C) -- variants with EE-chains, only for closing {cpcx-e,6} T[letrec X = nil; EE^A[Y,C[var X]]; E in S] ==> T[letrec X = nil; EE^A[Y,C[nil]]; E in S] where (var X, C) ,(var X, letrec EE^A[Y,dummy3[]] in HOLE) {cpcx-e,7} T[letrec X = (cons R1 R2); EE^A[Y,C[var X]];E in S] ==> T[letrec X = (cons (var Z) (var ZS)); Z = R1; ZS = R2; EE^A[Y,C[(cons (var Z) (var ZS))]]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) ,(var Y,letrec X=dummy3[] in HOLE) ,(var Z, T[letrec X = dummy3[]; ZS = dummy3[]; EE^A[Y,dummy3[]]; E in HOLE]) ,(var ZS, T[letrec X = dummy3[]; Z = dummy3[]; EE^A[Y,dummy3[]]; E in HOLE]) ,(T[letrec X = (cons R1 R2); EE^A[Y,C[var X]];E in S], letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,((cons (var Z) (var ZS)),C) {cpcx-e,8} T[letrec X = false; EE^A[Y,C[var X]]; E in S] ==> T[letrec X = false; EE^A[Y,C[false]]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) {cpcx-e,9} T[letrec X = true; EE^A[Y,C[var X]]; E in S] ==> T[letrec X = true; EE^A[Y,C[true]]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) {cpcx-e,10} T[letrec X = (pair[] R1 R2); EE^A[Y,C[var X]];E in S] ==> T[letrec X = (pair[] (var Z) (var ZS)); Z = R1; ZS = R2; EE^A[Y,C[(pair[] (var Z) (var ZS))]]; E in S] where (var X, C) ,(var X, letrec Y=dummy3[] in HOLE) ,(var Y, letrec X=dummy3[] in HOLE) ,(var Z, T[letrec X = dummy3[]; ZS = dummy3[]; EE^A[Y,dummy3[]]; E in HOLE]) ,(var ZS, T[letrec X = dummy3[]; Z = dummy3[]; EE^A[Y,dummy3[]]; E in HOLE]) ,(T[letrec X = (pair[] R1 R2); EE^A[Y,C[var X]];E in S],letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,((pair[] (var Z) (var ZS)),C) {abs,1} T[letrec X = (cons R1 R2); E in S] ==> T[letrec X = (cons (var Z) (var ZS)); Z = R1; ZS = R2; E in S] where (var Z, T[letrec X=dummy3[]; E in HOLE]) ,(var ZS, T[letrec X=dummy3[]; E in HOLE]) ,(T[letrec X = (cons R1 R2); E in S], letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,(Z,letrec ZS=dummy[] in HOLE) ,(ZS,letrec Z=dummy[] in HOLE) {abs,2} T[letrec X = (pair[] R1 R2); E in S] ==> T[letrec X = (pair[] (var Z) (var ZS)); Z = R1; ZS = R2; E in S] where (var Z, T[letrec X=dummy3[]; E in HOLE]) ,(var ZS, T[letrec X=dummy3[]; E in HOLE]) ,(T[letrec X = (pair[] R1 R2); E in S] , letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,(Z,letrec ZS=dummy[] in HOLE) ,(ZS,letrec Z=dummy[] in HOLE) {- not needed since, can be undone by ucp {abse,1} T[(cons R1 R2)] ==> T[letrec Z = R1; ZS = R2 in cons (var Z) (var ZS)] where (var Z, T[letrec ZS=dummy3[] in HOLE]) ,(var ZS, T[letrec Z=dummy3[] in HOLE]) ,(R1, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,(R2, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) {abse,2} T[(pair[] R1 R2)] ==> T[letrec Z = R1; ZS = R2 in pair[] (var Z) (var ZS)] where (var Z, T[letrec ZS=dummy3[] in HOLE]) ,(var ZS, T[letrec Z=dummy3[] in HOLE]) ,(R1, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) ,(R2, letrec Z=dummy3[]; ZS=dummy3[] in HOLE) -} {gc,2} T[letrec E in S] ==> T[S] where E /= {} ,(S,letrec E in HOLE) {gc,1} T[letrec E1;E2 in S] ==> T[letrec E1 in S] where E1 /= {} ,E2 /= {} ,[E1,letrec E2 in HOLE] ,(S,letrec E2 in HOLE) {ucp,1} T[letrec X=S; E in T1[var X]] ==> T[letrec E in T1[S]] where E /= {},(var X,T1),(S,T1),(letrec E in T1[dummy3[]], letrec X=dummy3[] in HOLE) ,(S, letrec X=dummy3[] in HOLE) {ucp,2} T[letrec X=S; E; Y=T1[var X] in S1] ==> T[letrec E; Y=T1[S] in S1] where (var X,T1) ,(S,T1) ,(letrec E; Y= T1[dummy3[]] in S1, letrec X=dummy3[] in HOLE) ,(S, letrec X=dummy3[] in HOLE) {ucp,3} T[letrec X=S in T1[var X]] ==> T[T1[S]] where (var X,T1),(S,T1),(T1[dummy3[]], letrec X=dummy3[] in HOLE) ,(S, letrec X=dummy3[] in HOLE)